How to pass 'current' value of a variable inside $past

nasim · Senior Joined: Nov 03, 2005 Posts: 15

Hi,

-------------------------------------
`define DELAY 5
bit [2:0] index;
bit [7:0] var;
...
...
a1: assert property (
@(posedge clk)
a |-> $past(var[$sampled(index)],`DELAY)
);
-------------------------------------

I want to write an assert property where I want to use the 'current' value of index to return value for a procedural variable for that index 5 cycles back, but I am unable to do that using $past (I can do it by creating a pipelined register of 5 stages, but I wanted to see if there is a nifty way of doing it inside the SVA itself).

At first, I had
$past(var[index],`DELAY));
but the simulator used the value of index 5 cycles back and returned the value of var for that index, i.e. it returned "var[index 5 cycles back]" instead of "var[current index] 5 cycles back".

Same thing happened when I explicitly used $sampled(index), i.e.
$past(var[$sampled(index)],`DELAY));
(also shown at the beginning of this post)
[I suppose $sampled's usage is limited to $displays inside action blocks]

And I don't think local variables will work either.
Does anybody know if there is a nifty way to do it?

Thanks.

Ajeetha

edcerny · Posted: Mon May 07, 2012 7:53 am **Post subject:**

Unless you store the entire array for 5 cycles, I do not see how you could select the variable with the current index value.

nasim · Senior Joined: Nov 03, 2005 Posts: 15

Thanks, Ajeetha.

I used $past outside of the SVA like you said and am getting the job done for now.
Here is the small testcase I used to play around with (reduced DELAY to 2 for quick testing purposes):

-----------------------------------------------------------------
`define DELAY 2
`define TRUE 1
`define POS @(posedge clk)

module test;
bit clk;
initial forever #1 clk=!clk;

bit a;
bit [2:0] b;
bit [7:0] x;

always `POS
$display("@%0t, a:%b, b:%d, x[%d]:%h, \$past(x[%d],1):%h, \$past(x[%d],2):%h, \$past(x[%d],3):%h",
$time,a,b,$sampled(b),x[$sampled(b)],$sampled(b),$past(x[$sampled(b)],1),$sampled(b),$past(x[$sampled(b)],2),$sampled(b),$past(x[$sampled(b)],3));

initial
begin
`POS; x=8'h0;
`POS; x=8'h1;
`POS; x=8'h2;
`POS; x=8'h3; a=1; b=1;
`POS; x=8'h4; a=0; b=2;
`POS; x=8'h5;
`POS; x=8'h6; a=1; b=3;
`POS; x=8'h7;
`POS; x=8'h8; a=0; b=4;
`POS; x=8'h9;
`POS; x=8'ha; a=1; b=5;
`POS; x=8'hb;
`POS; x=8'hc; a=0; b=6;
`POS; x=8'hd; a=1; b=7;
`POS; x=8'he; a=0; b=8;
`POS; x=8'hf;
`POS; x=8'h0;
$finish(2);
end

a0: assert property (`POS $rose(a) |-> $past(x[$sampled(b)],`DELAY));

property p1(v); $rose(a) |-> $past(x[(v)],`DELAY); endproperty
a1: assert property (`POS p1($sampled(b)));

// THIS ONE WORKS!!
logic [7:0] y;
assign y=$past(x,`DELAY,`TRUE,`POS);
a2: assert property (`POS $rose(a) |-> y[b]);

endmodule
-----------------------------------------------------------------------------

edcerny · Posted: Mon May 07, 2012 12:26 pm **Post subject: past...**

Yes, you are storing the whole array for 5 cycles, it can get expensive if x is large.

nasim · Senior Joined: Nov 03, 2005 Posts: 15

Hi Ed,
I am not an assertion expert by any means, but in general, shouldn't the usage of something like

$past(x[$sampled(b)],N));

pass the 'current' sampled value of b even if going back N number of cycles? It looks like $past overrides $sampled and instead looks at the value of b N cycles back (as well as returning x[b] N cycles back).

I can understand
$past(x[b],N));
should behave that way, but putting $sampled should have worked I would think. Or the simulator should at least warn the user (at compile time) that such usage should be discouraged given the $sampled will have no effect.

-Nasim

edcerny · Posted: Mon May 07, 2012 1:18 pm **Post subject:**

Hi Nasim,

putting $sampled on the index woudl not change it, because it still shifts $past of the whole by N cycles. To do what you want, it is necessary to save the whole array and then select it using the current index value. This is because you cannot know at the time N cycles back what the value of the index will be at the current time.