SystemVerilog Assertion on $rose

SystemVerilog
, , ,
1

Hi everyone,

Quick question on $rose() function for SVA.
Given a property:

property s_a; 
    @(posedge clk) $rose(a) |=> b;

endproperty

Between two rising edges of the clk signal, if signal ‘a’ starts with 0, then changes to 1 then changes back to 0 before reaching the next rising edge of a clock, would the $rose(a) return True or False?

Best Regards,

Sangwoo

2

I think that if a rising_edge is formed between two rising edges, it will not run the rose function.

the signal “a” is checked transitions to a value of 1 on every positive edge of the clock. If the transition does not occur, the assertion will fail.

In your case, it will be fail.

3

Is this from a ChatGPT or clones? Answer seems wrong to me. Since OP said:

rising edges of the clk signal, if signal ‘a’ starts with 0, then changes to 1 then changes back to 0 before reaching the next rising edge of a clock,

SVA samples using clocking event, in this case posedge clk - so at both posedge-s the value of a is 0, hence $rose(a) should be false.

4

Yes, the answer was wrong, I just wanted to paste the answer I saw elsewhere for the same question and see people’s reaction, I agree with your opinion on the subject. I editted my answer like above.