Re: [sv-ac] Ambiguous return value for $past

Stuart,
 I believe that  in your example "(out == $past(q, 2,enable))"
  "out" gets the value of "q" at the previous 2nd cycle that had 
"enable" true at posedge clk.
  Thus, if enable==0 at all cycles except that in cycle 10 enable==1, 
and at cycle 15 enable ==1 and we're in cycle 22, then
  at cycle 22, "out" will have the value that "q" had at cycle 10. 
"enable" is expression 2 used as a gating expression for the clocking 
event.

 Ben Cohen
 http://www.abv-sva.org

 -----Original Message-----
 From: Stuart Sutherland <stuart@sutherland-hdl.com>
 To: sv-ac@eda.org
 Sent: Thu, 14 Apr 2005 01:28:13 -0700
 Subject: [sv-ac] Ambiguous return value for $past


 LRM 18.7.3 does not fully specify the return value of $past when the
 optional "expression2" is used. It states:

 -------------
 When expression2 is specified, the sampling of expression1 is performed
 based on its clock gated with expression2. For example,

 always @(posedge clk)
 if (enable) q <= d;

 always @(posedge clk)
 assert (done |=> (out == $past(q, 2,enable)) ;

 In this example, the sampling of q for evaluating $past is based on the
 clocking expression
 -------------

 There are two ambiguities, at least in how I read the LRM.

  First is the statement "the sampling of expression1 is performed based 
on
 its clock gated with expression2". Is the gating based on the current
  sampled value of expression2, or the sampled value of expression2 at 
the
 specified number of clock ticks in the past?

  Second, since $past is a function, and can also be called from 
procedural
  code, it must return a value for when the enabling expression is 
either true
  or false. The return value for when expression2 is true is clear, but 
the
  LRM does not define the return value for when the enabling expression 
is
 false. At least I didn't find a definition.

 Does anyone know the answers to these questions?

 Thanks,

 Stu
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Stuart Sutherland
 stuart@sutherland-hdl.com
 +1-503-692-0898