[sv-ac] comments on 1757

Hi Folks:

I have read through 1757.  Below are my comments.

Best regards,

John H.

2007-08-20
----------

. The proposal should be aligned to Draft3a and should say so at the top.

. Item h) can't be added without changing the structure of the language 
  introducing this list.  I have said before that we should probably 
  abandon the "counting" of the property forms (i.e., "There are seven
  kinds of property").

. I think that item h) should be better aligned with what already exists
  in this part of the LRM.  E.g., 

     property_expression --> property_expr

     expression --> expression_or_dist

  This description needs to explain what the phrase "reset expression" means.

. The Changes suggested to 16.12 do not explain any difference between
  the reset expression for an accept_on/reject_on and that of disable
  iff is tested.  In the case of item f), a forward reference to
  16.12.2 appears in 16.12.  It seems that a similar reference needs
  to be made to the proposed 16.12.3 so that it is clear that further
  normative information about these constructs appears later.

. Proposed 16.12.3.  I think that 

    but they use the sampled value of their argument 

  should be made clearer.  I think a phrase like "reset expression" should
  have been introduced in 16.12 to refer to "b" in "accept_on (b) p" or
  "reject_on (b) p".  I think that then

    but they use the sampled value of their reset expression

  will be clearer.

. Throughout, semantics are --> semantics is, except in case two or more
  semantics are being referred to.

. I think that the reset expression of a disable iff is evaluated at a finer
  granularity than a simulation timestep.  My understanding is that if the 
  reset expression of a disable iff becomes true in any region of a timestep
  (e.g., reactive), then it affects all evaluation attempts in progress that 
  are governed by the disable iff (including, e.g., those that started
  the previous observed region).  I believe that also the disable iff is 
  sensitive to glitches within a timestep

. "For example, a sequence ... may be asserted".  This is not a sequence 
  property.  I understand that the antecedent is the sequence, but I think
  that this should be reworded for clarity.  Also, some phrase like 
  "may be asserted as" should be use to connect this description with 
  the displayed code. 

. "reject_on (or accept_on) that appear in nested properties are applied to the 
  inner most property first"  What happens with 

     accept_on (b) reject_on (b) 1[*0:$] ##0 0

  ?  Saying that they are applied to the "inner most property first" seems to
  contradict what is said later, that the "outermost operator takes precedence".

  I think that these paragraphs need to be reworked for clarity.  The notion
  of "before the inner property completes" needs to be more precise.  In the 
  intereting cases, the inner property is completing in the same timestep
  that the reset condition becomes true, and the proposal seems to be saying 
  that in such cases the reset condition wins.

. Paragraph beginning "Like disable iff, reject_on and accept_on expressions
  can contain" ... Avoid "like".  This needs to be reworked for LRM-ease.

. "legal deployment of the operators" is unusual.  I think that 

     The following recursive property declaration illustrates legal usage 
     of the accept_on and  reject_on constructs:

  is better.

. Changes to F.3.3.1.  If reject_on is derived, then an independent definition
  of its semantics should not be given here.
 
  I don't think it is necessary to restrict i to be the _least_ index such that 
  w^i |= b.  This should work for any such i.

  I don't understand why both formal and informal definitions are being given here.
  The English paragraphs can be remarks, but as they stand they are confusing 
  because it seems that two independent definitions are being given for the
  same concept.


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