[sv-ac] comments on 1932

Review 2007-11-20
-----------------

(Clause 16 changes through 16.12.9)

* Paragraph beginning "The result of property evaluation"
  - commas should not be set in bold courier
  - comma missing after "strong"
  - comma missing after "accept_on"
  - "and" after "until" should not be set in bold courier
  - I'm not sure about "if-else".  This string is not itself a keyword, but the
    substrings "if" and "else" are.  In 12.4, "if-else" is not in courier bold.
    I think this is the way the editor is going.
  - "followed_by" is not a keyword, so it should not be in courier bold.
    I recommend roman "followed-by" (note the hyphen instead of underscore) here 
    and throughout.


* In Table 16-25, numerous operators are incorrectly capitalized.

* According to the syntax, "strong" and "weak" require parentheses.  This
  implies that their operator precedence is not so important because the
  parentheses will determine the operand.  However, in placing these operators
  in the precedence table, we should look forward to what will happen if 
  the requirement on parentheses is relaxed.  My vision is that we will 
  eventually allow "strong" and "weak" to be applied to property expressions.
  Their current place in the precedence table makes them the highest precedence 
  among operators that can be applied to properties, which seems good to 
  me.  However, I do not understand the motivation behind placing them 
  between the linear and branching sequence operators.  Removing the 
  parenthesis requirement makes 

     r |-> strong a[*1:$] ##1 b and !c throughout d[->1]

  parse as

     r |-> strong(a[*1:$] ##1 b) and (!c throughout d[->1])

  Does it make better sense to move "strong", "weak" all the way to the highest
  precedence among sequence and property operators?

* I don't understand the rationale for making "accept_on", "reject_on" higher 
  precedence than the temporal operators.  Would these be better at lowest 
  precedence?

* I guess that the relative precedence for next, always/eventually, until is
  motivated from PSL.  I don't understand the rationale.

* In Table 16-25, "implies" and "iff" should be in bold courier and not 
  capitalized.

* Text following Table 16-25.  I am a little worried that this text is 
  being changed by 1648 to use "disable condition" rather than "reset expression".
  Can this text be aligned to show the changes from 1648, and identify these as
  changes consistent with 1648?

* 16.12.1, I think that "sequence_expr" should be in roman italic not courier
  or courier italic.

* 16.12.1, change sequence --> sequence_expr in

     strong(sequence_expr) evaluates to true if, and only if, there is a
     nonempty match of the sequence.

  Rationale:  The referent of "sequence" is ambiguous.

* 16.12.1.  I don't think the phrase

     there is no finite prefix that witnesses a non-match of the sequence
 
  is clear enough.  We will not be able to make this completely clear because
  of subtleties regarding contradictions (boolean, related to length incompatibility
  in intersect, etc.).  I recommend something like

     there is no finite prefix over whose evaluation the sequence_expr is demonstrated
     not to be able to match.  A more precise definition is given in [make a reference
     to the appropriate place in Annex F].

* 16.12.1, second paragraph.  There are distracting outer parentheses areound 
  weak(sequence_expr), weak(first_match(sequence_expr)), etc.

* 16.12.1, third paragraph, first sentence.  Make "verification statements" singular.

  Rationale:  The next sentence talks about "statement" in the singular.

* 16.12.1, third paragraph, second sentence,

     it is evaluated -->  the sequence_expr shall be evaluated

  Rationale:  Clarity, LRM-ese.

* 16.12.1, third paragraph, second sentence,

     otherwise it is being evaluated as --> otherwise it shall be evaluated as

* 16.12.1, examples involving p3.  
  - The discussion of p1 and p2 could be placed before the presentation of p3,
    c1, a1 and their discussion.  This is not critical, but a suggestion.
  - The indentation of c1, a1 is distracting.
  - The sentences

       The cover property c1 says that clk must rise at least once and that a is
       true when clk rises for the first time. The assertion a1 says that if clk
       rises at least once, then a must be true when clk rises for the first
       time.

    are confusing because the "cover property" and "assert property" can have 
    multiple attempts.  These sentences are really describing the dispositions
    of individual attempts.  I recommend rewriting as

       An evaluation attempt of the coverage statement c1 succeeds if, and only if, 
       clk rises at least once and a is true when clk rises for the first time. 
       An evaluation attempt of the assertion statement a1 succeeds if either clk
       does not rise or clk rises at least once and a is true when clk rises for 
       the first time.

* 16.12.1.  

     The not operator switch 

     --> 

     The not operator (see [add appropriate reference]) switches

  Also, make "not" bold courier.

* 16.12.1.  Avoid using the same labels within a subsection for different
  examples.  Change

     a1:  assert property (not a ##1 b);

  to

     a2:  assert property (not a ##1 b);

* 16.12.1.  Change

     This means that at the last cycle of a simulation the sequential property 
     a ##1 b always holds and thus, the assertion a1 always fails.

  to

     This means that if a holds in the last cycle of a simulation, then a ##1 b
     also holds as a weak sequential property in the last cycle, and thus the 
     assertion a2 fails.

  Rationale:  It is not true that a ##1 b always holds in the last cycle of 
  a simulation.

* 16.12.8.  I think there should be a reference here to the rewriting algorithm 
  of 1549.  Also, I think there should be a reference to the section on multiclock
  rules.

* 16.12.9.  "followed_by" is not a keyword, so it should not be in courier bold.
    I recommend roman "followed-by" (note the hyphen instead of underscore) here 
    and throughout.

* 16.12.9.  In the syntax box, there is a space missing after #-#.

* 16.12.9, sentence after the syntax box.  The referent of "this clause" is
  ambiguous.  I recommend changing to "this construct" to match the word used
  in the preceding sentence.

* 16.12.9, second bullet explaining semantics.  "property_expr" and "sequence_expr"
  should be roman italic.

* 16.12.9.  There are some font inconsistencies with courier vs. roman italic 
  for sequence_expr and property_expr.  I can see some of the reasons why 
  different fonts are being chosen for references in "code-like" examples vs.
  references to syntax non-terminals in text.  I'm not sure what to do about
  this.

* 16.12.9.  The examples p1, p2 reference "always".  I think that this is
  a forward reference, so consider adding a cross reference.

* 16.12.9, next-to-last paragraph.  Remove period before "Note".  I think
  that notes are not normative and may require special setting.  Try to 
  reword without using "note".

* 16.12.9, last sentence.  "followed_by" in italic is unusual.  Make this 
  consistent with other references to the term.


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