[sv-ac] comments on 1674

All:

I had a look over 1674 in preparation for calling for a vote.

I think a few things need to be fixed first.

Please see below.

J.H.


notes 2007-06-11
----------------

. The proposal needs to be aligned to Draft 3 numbering.  I think
  17.14.6 should be 16.14.6 and later subsubclauses need to be
  renumbered.

. Change 

     The inferred disable expression is the reset expression from the
     default disable expression (See 17.14 Note to editor: This is
     after introducing proposal #1648). If there is no default disable
     expression defined, the function $inferred_disable returns false.

  to 

     The inferred disable expression is the disable condition from the
     default disable declaration whose scope includes the call to
     $inferred_disable (See 16.15 Note to editor: This is after
     introducing proposal #1648).  If the call to $inferred_disable is
     not within the scope of any default disable declaration, then the
     call to $inferred_disable returns 1'b0.

  Rationale: Improved clarity and alignment to the language of 1648.
  Also, to my knowledge "false" is not defined as an expression in
  SystemVerilog, so I think it makes better sense to say that the call
  to the system function returns "1'b0".

. Change 

     then the cumulative condition is true (i.e., 1'b1).

  to

     then the cumulative condition is 1'b1.

  Rationale: I don't think that "true" is defined as an expression in
  SystemVerilog.

. I am not sure if a call to an inferred expression function is allowed
  to be a proper subexpression of the default value expression for a 
  formal argument.  I assumed not, in which case I recommend the following
  change for clarity:

     An inferred expression function may only be used as the default
     value on a formal argument to a property or sequence, not within
     the body of an expression. When an inferred expression system
     function is used as the default value on a formal argument to a
     property or a sequence, it is replaced by the inferred expression
     as determined at the point where the property or sequence is
     instantiated.

  to

     A call to an inferred expression function may only be used as the
     entire default value expression for a formal argument to a
     property or sequence declaration.  A call to an inferred
     expression function shall not appear within the body expression
     of a property or sequence declaration.  If a call to an inferred
     expression function is used as the entire default value
     expression for a formal argument to a property or sequence
     declaration, then it is replaced by the inferred expression as
     determined at the point where the property or sequence is
     instantiated.

  If my assumption is not correct, then much of the above will still
  work for clarity, but "be/is used as the entire" should be "be/is
  used in a" or something similar.
  

. For clarity, I recommend changing

     Therefore, if the instance is the top expression in a
     verification statement, the event expression that is used to
     replace the default argument $inferred_clock is that as
     determined at the location of the verification statement. If the
     instance is not the top-level property expression in the
     verification statement then the event expression determined by
     clock-flow rules up to the instance location in the property
     expression is used as the default value of the argument.

  to

     Therefore, if the property or sequence instance is the top-level
     property expression in a verification statement, the event
     expression that is used to replace the default argument
     $inferred_clock is that as determined at the location of the
     verification statement. If the property or sequence instance is
     not the top-level property expression in the verification
     statement then the event expression determined by clock-flow
     rules up to the instance location in the property expression is
     used as the default value of the argument.


. There is a font problem with the "|=>" operator in the declaration
  of p_triggers.  The same font problem occurs in assertions a1, a2, a3 of 
  the second module m.

. Check the font of the tick in the '0 actual argument to p_triggers in a2 of
  the first module m.  Also, why is there a difference between this and
  the expression 1'b0 in the disable in a2 of the second module m?  I recommend
  making these expressions identical.  We are not trying to illustrate
  constant equivalences in this example, so the difference is noise in my
  opinion.

. "rst" is not declared in module m.  This makes it hard to judge 
  whether a3 in the first module m is equivalent to a3 in the
  second module m.  If rst is 4-valued, then I don't think the two 
  are equivalent because of the 4-value negation problem that we have
  been discussing with other mantis items.  I think !rst needs to be
  changed to something like !bit'(rst!='b0) as in the proposal for
  1648.  Also, the text at the end that talks about the inferred 
  enabling condition for a3 needs to be changed.

  It is o.k., although somewhat subtle, that the second form of a3 does
  not have to include the inferred enabling condition as precondition, 
  i.e.,

     a3:  assert property
     (
        @(posedge clk2) disable iff (rst1)
        (!bit'(rst!='b0) && d) |-> 
        (!bit'(rst!='b0) && d) throughout (a ##0 b[->]) |=> c
     );

  This is accidental because of the form of the property.

  Also, note that "b[->]" needs to be changed to "b[->1]".

. In the a4 in the second module m, why is there a second "@(posedge clk1)"
  just before "d"?  This is not wrong, but it is not needed and I find it
  distracting since the substitution into the form of p_multiclock
  does not yield it.

. Change

     instancein the assertion

  to 

     instance in the assertion

. Consider changing '1 to 1'b1 in the last paragraph.


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