[sv-ac] Comment regarding LTL - Mantis 1932

Hello John,

please see my comments regarding the proposal for Mantis 1932 - LTL.

Best regards,
ed

----

pp5, first par. after WITH, 2nd sentence: Perhaps this should be placed
after the discussion about disable iff.

pp6, bottom par.: here and in other places Except in simulation
semantics, we use "simulation cycle", but that is nowhere defined, as
far as I could tell. Perhaps it should be "simulation time slot"?

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.
 
pp8, top text should be moved to the end of 16.12.2, i.e.,
The not operator switches the strength of a property. In particular one
should be careful when negating a
sequence. For example consider the following assertion:
a1: assert property (not a ##1 b);
Since the sequential property a ##1 b is used in an assertion, it is
weak. This means that if a holds at the last
tick of the assertion's clock in a simulation, the weak sequential
property a ##1 b will also hold beginning at
that tick, and so the assertion a1 will fail. In this case it is more
reasonable to use:
a2: assert property (not strong(a ##1 b));
 
should be moved at the end of the clause on negation.
 
pp9, 16.12.9: The names of property kinds are bold, e.g., followed_by,
but these ar not keywords. Should it be simply in italic or regular
text, but I do not think it should be like a keyword. This applies to
all the subsequent clauses defining operators. Also, perhaps it should
be written as followed-by.
 
pp9, followed by: "The clause is used to precondition monitoring..."
perhaps it should read "The clause is used to trigger monitoring ..."?
 
pp9: replace "The following points should be noted for #-# followed_by:"
by "For the followed-by property to succeed, the following must hold:"
Also, the 3rd bullet seems redundant, just explains the first two
bullets. Perhaps that one should be written as a note?
 
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.
 
pp11, Examples: The comments should start with "property succeeds if
...", otherwise it is not clear what is being described. 
 
pp11, 12, Examples: Many keywords or parts thereof are not in bold. 
 
pp13, top example: the label explicit_always: should not be bold.
 
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.
 
pp14, 15, Examples: keywords should be in bold font.
 
pp14, description of examples: The equivalent in terms of sequence
operators for p4 is true only if a is a boolean and b a sequence or
boolean. Perhaps it should be stated.
 
pp15, 16, description of examples: a would have to be a sequence or
boolean for the equivalent form of p1.
 
pp16, 16.12.15, 1st par., 3rd line: "... that the property clock ticks
enough...
 
pp18, bottom: if / if else should be in bold.
 
pp19, middle of page: keywords should be in bold.
 
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)
 
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.
 
------------------------
 
 
 

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