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.
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);