RE: [sv-ac] comments on 1757

Hi John,

Please, see my comments regarding disable iff.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Tuesday, August 21, 2007 4:46 AM
To: sv-ac@server.eda-stds.org
Subject: [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

[Korchemny, Dmitry] I don't think that disable iff has well defined
simulation semantics at all. My understanding is that disable iff uses
the value of the reset available in the observed region. I still think
that it should use sampled values, but should not be sampled by the
(leading) clock. 
The difference between disable iff and accept_on/reject_on should be
that disable iff defines the main reset of the assertion, and when it is
high, we have a disabled computation of an attempt, while
accept_on/reject_on are just temporal operators. In FV it means that
disable iff has accept_on semantics in assertions and assumptions, and
reject_on semantics in cover directives.

. "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.

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