Can I access delayed value in SystemVerilog assertion

Question

I want to use an old value of a signal in a SystemVerilog assertion.

This is what I am currently doing

logic [ADDRESS_WIDTH-1:0] old_address [1:0];

always_ff@(posedge rdclock) begin
   old_address[0] <= rdaddress;
   old_address[1] <= old_address[0];
end

property FooBar;
   @(posedge rdclock) rden |-> ##2 q == mem[old_address[1]];
endproperty

Baz: assert property (FooBar);

Is this how is should be done, or can I somehow use an old version of rdaddress directly in the assertion?

Answer 1

You can use the $past(...) system task. Using $past(rdaddress) will return the value of rdaddress that was sampled in the previous cycle. You can specify how many cycle in the past to go with the second argument. In your case, calling $past(rdaddress, 2) will return the value of rdaddress 2 cycles before.