Assertion to check signal asserted for only one clock cycle

In reply to ben@SystemVerilog.us:

Hi Ben, Thank you for sharing your understanding.


property sva_p2;
  @(posedge clk) $rose(signal) |-> @(negedge clk) $fell(signal);
endproperty

I tried this assertion “sva_p2” and it is working perfectly fine even with the cases mentioned above…
As our expectation, both cases are failing…

But now the question is that, Is the assertion “sva_p2” can be considered correct, As it is having posedge and negedge event of the same clock…

Waiting for your insight on the same,
Thank You,
Dhruvesh.B