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

Stuart,

I think Ben is right. Just to answer your second question, if value
of $past is used in procedural code when enable is not true, it will
return the $past value when last time enable was true. Based on Ben's
example, $past will return the same value at cycle 22 and after that
until enable becomes true again. 

As per current LRM, "If the specified clock tick in the past is before
the
start of simulation, the returned value from the $past function is a
value of
X". This statement seems to be incorrect as the return value should be
whatever is the initial value of expression1 (as value of X does not
make
sense for two state logic).

This is based on my current understanding of LRM.

Thanks.
Manisha

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
vhdlcohen@aol.com
Sent: Thursday, April 14, 2005 7:04 AM
To: stuart@sutherland-hdl.com; sv-ac@eda.org
Subject: 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