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