how to write assertion for asynchronous reset behavior

Question

Lets take a simple example of a d flip flop with asynchronous reset.

q should be updated with d on next edge of clock, this can be written with simple implication operator assertion.

However how to capture reset behavior in assertion. I've tried following few

assert @(posedge rst) (1'b1 |-> !Q);

assert @(posedge rst) (1'b1 ##0 !Q);

both these assertions fail, I think because there is no next posedge of rst?

assert @(posedge clk) ($rose(rst) |-> !Q);

passes but requires free running clock and is asserted between 2 edges of clock (not ann inteded behavior for rst)

 assert #0 (not (rst & Q));

As per my understanding this is a correct immediate assertion, however I can't see this one passing / failing in waveform viewer. Further more I think I won't be able to write cover on last type of assertion.

Answer 1

The assertions fails because Q is sampled before it is updated. Sampling happens on the LHS of the triggering event, early in the simulator's scheduler. Q is updated in the reactive region which is later in the scheduling order.

An easy way to correct this is to add a tiny delay such as SystemVerilog's 1step. I suggest putting rst in the checking condition that can work as a part of a minimum pulse-width check.

wire #(1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);

If you are simulating with a reset-to-q delay, such as from with SDF annotation or artificial delay, then add the offset to rst_delay.

wire #(r2q+1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);