Behaviour of $rose in SV Assertions

SystemVerilog
, ,
1

Hi All,

I have a query regarding the behaviour of $rose in SVA. I have a property as shown below:

property example;
@(clk) rose(signal1) |-> first_match(##[2:5] signal2 == 1) ##1 ((signal2 == 1) [*1:] ##1 ($rose(temp_bit)));
endproperty

Here signal1 is not aligned with either of the edges of the clock. Infact signal1 rises somewhere between the negative and positive edge of the clock. Still the property starts evaluating from the the nearest positive edge of the clock. Can anyone help me understand this behaviour?

2

In reply to atanubiswas:

property example;
@(clk) rose(signal1) |-> first_match(##[2:5] signal2 == 1) ##1 ((signal2 == 1) [*1:] ##1 ($rose(temp_bit)));
endproperty

$rose gives out an boolean value by checking whether the signal had risen from previous edge(whatever is given) to the current edge. When you say $rose(a), it gives 1 or 0. It gives 1 if signal value was 0 at previous edge and it is 1 at this/current edge.

.
In your case, All these signal’s values are sampled at change of clk (both posedge and negedge) as mentioned in assertion @(clk).
Signal1 is changing between negative and positive edge of clk. so it see the signal1 high at positive edge of the clock so it start evaluating from that positive edge of the clock.