Difficulty: Medium · Puzzle 6 of 6 · Topic: Event Scheduling Puzzles
The assertion fails and its action block drives req<=0. Decide whether that can fix the same failing edge, how many times the assertion fails, and what ack and req are at the end of the t=5 slot.
`timescale 1ns/1ns
module tb;
bit clk = 0;
bit req = 1;
bit ack = 0;
always #5 clk = ~clk;
always @(posedge clk) ack <= req;
ap_same_cycle: assert property (@(posedge clk) req |-> ack)
else begin
req <= 0;
$display("[%0t REACTIVE] action drives req<=0", $time);
end
always @(posedge clk)
$strobe("[%0t] end of slot req=%0b ack=%0b", $time, req, ack);
initial begin
repeat (3) @(posedge clk);
#1 $finish;
end
endmoduleThe assertion samples in Preponed; the action block runs later, in Reactive, after the sampled values are fixed.
1) At t=5 the preponed samples are req=1 and ack=0, so req |-> ack fails.
2) Meanwhile the always block (Active) already executed ack<=req with req=1, so ack becomes 1 in the t=5 NBA region.
3) The action block runs in Reactive and schedules req<=0. It cannot change the already-taken sample, so the failure at t=5 stands.
4) End of the t=5 slot: req=0 (from the action block) and ack=1 (from the Active read of req=1).
5) At t=15 and t=25 req is 0, so the antecedent is false and the property passes vacuously. Total failures: one, at t=5.Answer: No. The assertion fails exactly once, at t=5; the action block only changes later behaviour. After t=5: req=0, ack=1.
Checked by running the code in Verilator 5; the printed output supports the answer above. The action block fires once, at t=5, and cannot undo that failure; after t=5 the antecedent is false.
Treating the action block as if it ran in Active, or as if it could undo the sampled failure, is the trap. Also do not confuse the two reads of req: the DUT read it in Active (1), the assertion read it in Preponed (1), the action write lands last.
How would you encode a non-overlapped check that matches this pipeline behaviour? Model answer: assert property (@(posedge clk) req |=> ack); ack is req delayed by one clock, so the check passes at every edge here.
No, the action block cannot rewind the edge. The assertion sampled req equal to 1 and ack equal to 0 in Preponed, so it fails once at five, and the action block runs later in Reactive. Its write sets req to 0 while the DUT had already copied req of 1 into ack, so after the slot req is 0 and ack is 1. The trap is thinking the action block runs in Active or can undo the sample; I would check that later edges pass only vacuously, which is a coverage worry.