I am trying to understand when to use $rose
for a signal in assertion. For instance in what ways the two below assertions will behave differently?
first:assert property
(@(posedge clk) $rose(reset) |-> (data == 0));
second: assert property
(@(posedge clk) reset |-> (data==0));
is it that $rose
is to be used with asynchronous signals?
$rose
means that in the previous clock cycle the signal was '0' and in the current clock cycle it is '1'.
The first assertion will only check on the first cycle when reset
goes high, whereas the second assertion will check that data
is '0' in every clock cycle when reset
is high.
Here's a nice drawing showing you when each of the assertions will trigger.
_ _ _ _ _ _
clk _| |_| |_| |_| |_| |_| |_
___________
reset _____| |_______
first x
second x x x
$rose
has meaning for synchronous signals.