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'.

2) $past is used to replace the need for auxilairy variables, that is:

$past(a, 1, clk)

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 agree with Bassam that the flexability is required since we may have auxilairy variables with different clock domains,

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.
> > 
> > 
> > 
>