RE: [sv-ac] comments on 1674

Hello John and all,

please find attached an updated (and hopefully w/o errors) proposal.
Also uploaded.

did not replace true/false by 1'b1/1'b0, just added both. true / false
are already used in several placesm e.g., 16.3, 16.8.3, etc.

Best regards,
ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John Havlicek
> Sent: Tuesday, June 12, 2007 11:53 AM
> To: sv-ac@eda-stds.org
> Subject: [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.
> 
> 

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