Is it legal to write something like below - I didn’t find anything against this in LRM
works on major 3 simulators though.
want to check, if there was a rising edge on a particular signal 3 clocks early
property ack_chkr;
@(posedge clk)
$rose(ack) |-> $rose($past(req,3));
endproperty
irony is even $past($rose(…)) seems to work
In reply to ssureshg_:
It’s legal based on the syntax.
In general, it’s better to write forward looking, cause /effect, types of properties.
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
There are cases where one may want to assert that if there is an effect it is because of a cause (or one of possible causes).
For example, one would assert that you only get gnt if there was a req.
You don’t want to see a spurious gnt.
One could use the $past, but the number of cycles of the past has to be static, no range. For that case of a range, asolution is to use support logic that latches (store) the event of a req and resets it with the gnt.
You can then assert something like
not(gnt && req_latch==0); // property body
Ben systemverilog.us