Assertion race condition

SystemVerilog
1

I have the following assertion:

REQ_ACK_DELAY_0_TO_6: assert property (@(posedge _clk) (_req && (!disable_assert_check)) |-> ##[0:6] _ack);

  • _req is a one-cycle pulse, asserted at time t1 (i.e., at the posedge of _clk).
  • _ack comes after 7 cycles (i.e., at t1 + 7) in simulation (VCS).
  • However, the assertion is not failing, even though it should — _ack is clearly outside the expected [0:6] window.

Interestingly, the following assertion does fail in this case:

REQ_ACK_DELAY_0_TO_6: assert property (@(posedge _clk) (_req && (!disable_assert_check)) |-> ##[0:5] _ack);

Also, the version using $rose(_req) like this:

assert property (@(posedge _clk)
disable_assert_check == 0
&& $rose(_req)
|-> ##[1:6] _ack
);

correctly catches the violation and behaves as expected.

2

Please share an EDA link for the same