RE: [sv-ac] SVA - $sampled

 
> 
> 1) We need a way to initialize the initial value of $past, 
> for example if we were to create a counter example from a 
> formal tool we could not give an 'x'.

Yes, that would be helpful, but may be needed for $rose, $fell,
$sampled, $stable too.
Currently the only way to avoid false failures in assertions is to use a
reset for at least one clock tick.

> 
> 2) $past is used to replace the need for auxilairy variables, that is:
> 
> $past(a, 1, clk)

Should be $past(a, 1, @(posedge clk) for your example.

> 
> Needs to be equivalent to a_d1:
> 
> reg a_d1;
> always @(posedge clk)
>  a_d1 <= a;
> 
> With the current scheduling semantics it seems that it is 
> not. Can we redefine the evaluation semantics of $past 
> according to the above.

I believe that the way it is defined is OK, or more precisely, it is
equivalent to

 reg a_d1;
 always @(posedge clk)
  a_d1 <= $sampled(a);

which is the same as what you wrote if there is no critical race.


> 
> I agree with Bassam that the flexability is required since we 
> may have auxilairy variables with different clock domains,

Yes.

Best regards,
edd

> 
> Thanks
> 
> 
> 
> Hillel Miller>
> 
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Eduard Cerny
> Sent: Wednesday, May 10, 2006 10:41 PM
> To: Bassam Tabbara
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] SVA - $sampled
> 
> I am not sure that keeping the clocking event gives any 
> flexibility, actually it is more ocnstraining and can cause problems. 
> 
> ed
> 
> 
> > -----Original Message-----
> > From: Bassam Tabbara
> > Sent: Wednesday, May 10, 2006 2:35 PM
> > To: Eduard Cerny; 'Eduard Cerny'; 'sv-ac@eda.org'
> > Subject: RE: [sv-ac] SVA - $sampled
> > 
> > Ok, may be some clarification is in order (emphasize the 
> preponed bit) 
> > then, and strike out the misleading "first occurrence of 
> clock" bit -- 
> > that should be covered by SV in fact it bugs me now for some types 
> > (int) X has no meaning whereas 0 does. Unless I am grossly 
> taking this 
> > out of context it is actually a wrong statement.
> > 
> > But the clocking part is already optional so leave that flexibility 
> > in.
> > 
> > Thx.
> > -Bassam.
> > 
> > -----Original Message-----
> > From: Eduard Cerny
> > Sent: Wednesday, May 10, 2006 11:27 AM
> > To: Bassam Tabbara; Eduard Cerny; sv-ac@eda.org
> > Subject: RE: [sv-ac] SVA - $sampled
> > 
> > My point is that the clock is not needed and if you do use 
> the clock 
> > explicitly it is not clear what you get. It would depend on whether 
> > you evaluate the function before or after the clock tick happens in 
> > the same time step. E.g., in a continuous assignment.
> > 
> > ed
> > 
> > > -----Original Message-----
> > > From: Bassam Tabbara
> > > Sent: Wednesday, May 10, 2006 2:21 PM
> > > To: Eduard Cerny; sv-ac@eda.org
> > > Subject: RE: [sv-ac] SVA - $sampled
> > > 
> > > Ed I am missing something here:
> > > 
> > > A) clock is already optional (and can be inferred from context)
> > > B) It is mostly understood that all these functions always
> > sample in
> > > preponed (whether inside or outside) assertion context.
> > > 
> > > So I claim this is largely not needed -- ??
> > > 
> > > Thx.
> > > -Bassam.
> > > 
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of 
> > > Eduard Cerny
> > > Sent: Wednesday, May 10, 2006 11:14 AM
> > > To: sv-ac@eda.org
> > > Subject: [sv-ac] SVA - $sampled
> > > 
> > > Hello,
> > > 
> > > while discussing Dmitry's comments regarding the sampled value 
> > > functions $rose, $past etc., I think we should also review the 
> > > definition of $sampled as outlined below. If you agree 
> that this is 
> > > useful I will enter it in Mantis.
> > > 
> > > Best regards,
> > > ed
> > > 
> > > ----------------------
> > > 
> > > Currently $sampled is defined as follows:
> > > 
> > > ---
> > > $sampled(expression [, clocking_event])
> > > 
> > > Function $sampled returns the sampled value of the 
> expression with 
> > > respect to the last occurrence of the clocking event. When
> > $sampled is
> > > invoked prior to the occurrence of the first clocking
> > event, the value
> > > of X is returned. The use of $sampled in assertions,
> > although allowed,
> > > is redundant, as the result of the function is identical to the 
> > > sampled value of the expression itself used in the assertion.
> > > ---
> > > 
> > > The use of this function outside of assertions and 
> assertion action 
> > > blocks is rather difficult.
> > > 
> > > Yet it is useful in assignments to auxiliary state variables of 
> > > assertions, once changed as follows:
> > > 
> > > ---
> > > 1) Remove the clocking event:
> > > 
> > > $sampled(expression)
> > > 
> > > 2) Change the description to:
> > > 
> > > Function $sampled returns the value of the expression at
> > the prepone
> > > time of the current simulation time unit.
> > > ---
> > > 
> > > With this definition, it is possible to have
> > > 
> > > reg auxiliary_state;
> > > 
> > > always @(posedge clk)
> > >    auxiliary_state <= funct($sampled(some_input));
> > > 
> > > in which case the auxiliary_state is assigned the same
> > value as seen
> > > by an assertion over some_input.
> > > 
> > > 
> > > 
> > 
>