SVA : using $past

In reply to prashantk:

In reply to ben@SystemVerilog.us:
HI ben , I want to write an assertion for a signal “a” and “b” where the signal “a” is the exact replica of signal “b” just one cycle before.
I am implementing this : -
$rose(a) |-> $past(b,1); // width of both signals are exactly the same.
Correct me If I am wrong here , because I think this sequence is not checking the width of both signals rather ,only posedges of signals with a cycle of one delay.

  • $rose(a) |-> $past(b,1); is s property and is NOT a sequence
  • $rose(a_4bitbus) means that a_4bitbus went from 4’b0000 to something other than 4’b0000. Thus you would get a rose if a_4bitbus went from 4’b0000 to 4’b0001 or to 4’b1010 or 4’b0100 …
  • When you say $past(b,1), you are saying the in the last cycle “b” was not a zero
  • What you may want is something like
    $changed(a) |-> b==$past(b,1); // if “a” changed, then current “b”== past “b”
    Note the comparitor b==$past(b,1)

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