RE: [sv-ac] Comment regarding LTL - Mantis 1932

Hi Ed,

 

Thanks for the review

 

I implemented most of your comments. I do have some notes below

 

Doron

 


pp7, 16.122.1: "Since only one match of a sequence_expr is needed ..."
Also I am not sure why this and the next paragraph is needed.

 

[[DB:]] I fixed the typo, I think these paragraphs add intuition, so I
left them in.

 

 

pp10, 16.122.10: the text explaining the Examples is correct only if the
properties are in a verif. statement that is in an initial procedure.
That should be mentioned.

 

[[DB:]] I think that the correction for the next item should be enough

pp11, Examples: The comments should start with "property succeeds if
...", otherwise it is not clear what is being described. 

 

[[DB:]] I add "The comments in the following examples describe the
conditions for the properties to be evaluated to true." before the
examples

 

 

pp13, Examples: the description is only correct if these properties are
in verif. statements in initial procedures. Bottom of description
paragraph, always should not be bold, because it is a generic term
there.

 

[[DB:]] I add some text that say that the conditions described are for
the property to be evaluated to true

 

 

pp23, b): 

 Every explicit semantic leading clock of q1 [ else q2 ] is identical to
c.

 

is legal, but

@(c) if (b) @(c) (p1 else @(c2) p2)

 

[[DB:]] I think that the current text is fine. The first sentence sait
that both operands should be clocked with the leading clock

The seconf is illegal because the second operand of the "and" is clocked
on a different clock.

 

pp23: If p1 until p2 is the max. property of an assertion, it is not
clear whether the leading clock of p1 can be different of the clock of
p2. I'd say that the clocks shall be the same, but I could not see it
from the text.

 

[[DB:]] I am not sure what you mean. Why is it important whether this is
a top level property?

------------------------

 

 

 


-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.