How to use $past(array[index]) in assertion where index is from current cycle

SystemVerilog
,
1

I’m trying to use the value of an array element 4 cycles ago in an assertion, and for that I’m using $past. The index of the array is a variable and not a constant. So, when I use $past(array[index],4), I think the assertion is using the index also from 4 cycles ago. I instead want the array to be from the past (4 cycles ago), but the index to be the current value. I tried to use $sampled for the index but that didn’t really make any difference. I tried giving (##4 index) in place of index to compensate for $past for index, and that’s giving compile errors as I expected. Is there an easy way to get what I’m trying to achieve here? I can use always block and save a 4 cycle delayed version of the array (by latching the array), but the array is huge and it will end up using a lot of memory, which is probably not worth it for the sake of one assertion.

This is the simplified use case. Array is a 2D array below.
X |-> ($past(array[$sampled(index)],4) === 1)))

2

You could do something like the following:

module ary; 
    bit clk, x; 
    int ar[0:1023][0:1023]; 
    int index1, index2; 
    // X |-> ($past(array[$sampled(index)],4) === 1)))
    property p_x4;
        int v; 
            (1, v=ar[index1][4]) ##4 x |-> 1'b1;
    endproperty
    ap_x4: assert property(@ (posedge clk) p_x4); 
endmodule

Note;
(1, v=ar[index1][4]) ##4 1’b1 |-> x;
is not the same since if x==0, it a failure, whereas in above property p_x4,
if x==0, the assertion is vacuous, which is what you want.
Using the local variable to store the data you need is also efficient.

Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books