[sv-ac] 1932 comments

Hi Doron,

 

Here are my comments about the first part of the proposal
(LTL.1932.080123.pdf).

 

Most of them are minor editorial, a couple of comments are more
technical, but their fixing should be trivial. You can consider all the
comments as friendly amendments, but I am not voting since I haven't
reviewed the second part of the proposal (Annex F) yet.

 

General note. It looks like all the fonts are too small. E.g., the
normal text is in New Times Roman 8 instead of 10.

 

*	Page 2. The assertion examples in the motivation section should
be in black.
*	Page 3, second line "s_eventually", "s_" should be in bold.
*	Page 7.
	"Since only one match of a sequence_expr needed for
strong(sequence_expr) to hold, a poperty of the form
strong(sequence_expr) evaluates to true if and only if the property
strong(first_match(sequence_expr)) evaluates to true.

	*	"one match of a sequence_expr": "sequence_expr" should
be in italic.
	*	"for "strong(sequence_expr)"" : "()" should not be bold
	*	"poperty" -> "property".
	*	 "true" should not be italicized.

*	Page 7. "...and c is true..." c should not be bold.
*	Page 8. Assertions a1 and a2. ##1 should not be bold.
*	Page 8. "The not operator switches ..." need a reference to
16.12.2.
*	Page 8.
	"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:"

	*	Need to introduce a clock, say @clk in these examples.
	*	I prefer the explanation which would cover both
simulation and formal verification: "This means that if clk stops
ticking and a holds at the last tick of clk, 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:"

*	Page 9. "A property is a followed_by if it has one of the
following forms...". followed_by should be in regular italic (actually,
I am not quite confident, followed_by is a name like implication, and
implication is rendered in regular Times New Roman. One is clear, it
shouldn't be courier. Whatever you choose, be consistent throughout the
document: either use regular or italic Times New Roman.)
*	Page 9. Syntax diagram: #-# and #=# should be in red.
*	Page 9. Make uniform spacing between bullets.
*	Page 10. "Therefore, sequence_expr #=# property_expr is
equivalent to the following: sequence_expr ##1 1 #-# property_expr". I
don't think that these formulas are equivalent. The equivalent form
after clock rewriting is sequence_expr ##1 @11 #-# property_expr, but
this cannot be written in the body of LRM. I would drop this rewriting
note.
*	Page 10. "sequence_expr #-# strong(sequence_expr1)". "#-#"
should not be in bold.
*	Page 11. First line: "(indexed form of weak next )" --> :
"(indexed form of weak next)" - Drop a space.
*	Page 11. "either there are not const_expression clock ticks or
property_expr evaluates true" --> "to true".
*	Page 11. "only if, there exist const_expression clock ticks and
property_expr evaluates true" --> "to true".
*	Page 12. "A property is an always if it has one of the following
forms, which use the always operators:". "always should be in courier 9.
Check all other occurrences of this and other operators (until, etc.).
*	Page 13. "Implicit_always: assert property(p);" -->
"implicit_always".
*	Page 13. "initial explicit_always: assert property(always p);"
"explicit_always" should not be in bold.
*	Page 14. "clock tick exist at which property_expr2".
property_expr2 should be in regular courier 9 (same regarding next
occurrences of property_expr1 and property_expr2).
*	Page 14. s_until and s_until_with in the examples should be in
bold.
*	Page 14. "and that a shall be true": a should be in courier 9.
*	Page 14, at the bottom. "(ranged weak form of eventually)"
should be in Times New Roman.
*	Page 15, at the top. Same comment about "(ranged weak form of
eventually)".
*	Page 15, examples. All occurrences of "s_eventually" should be
in bold (sometimes only "eventually" is in bold).
*	Page 16. Delete "h)".
*	Page 20. "intersection, if-else, and the until": "and" should be
in Times New Roman.
*	Page 24. Note the list item numeration in the WITH clause
*	Page 25. 4). Insert values for accept_on and reject_on from
1751. Also in M.2 (page 26).
*	Page 25 #-# and #=# should not be in bold.

 

Thanks,

Dmitry


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