system-verilogsystem-verilog-assertions

when to use $rose system task with a signal in assertions


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?


Solution

  • $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.