Difficulty: Medium · Puzzle 1 of 6 · Topic: Event Scheduling Puzzles
On the first three rising edges, decide whether the assertion passes or fails. Explain why the result disagrees with the values you would read after the NBAs.
`timescale 1ns/1ns
module tb;
bit clk = 0;
bit a = 0, b = 0;
always #5 clk = ~clk;
always @(posedge clk) begin
a <= ~a;
b <= a;
$display("[%0t ACTIVE] a=%0b b=%0b", $time, a, b);
end
ap_align: assert property (@(posedge clk) b == a)
else $display("[%0t] FAIL: sampled b != a", $time);
initial begin
repeat (3) @(posedge clk);
#1 $finish;
end
endmoduleConcurrent assertions sample in preponed, not after NBAs.
1) At t=5 the preponed samples are a=0 and b=0, so the assertion passes. The always block then queues a<=1 and b<=0.
2) At t=15 the samples are a=1 and b=0 (the values left by the t=5 NBAs), so it fails.
3) At t=25 the samples are a=0 and b=1, so it fails again.
4) b is a one-cycle-delayed copy of a, so b == a can only hold on the first edge, when both are still 0.
5) The #1 before $finish keeps the t=25 evaluation (Observed region) from sharing a time slot with $finish, so every tool reports it.Answer: Pass at t=5, fail at t=15 and t=25. The assertion compares preponed samples (values from just before each edge), so it sees the previous-cycle relationship, never the post-NBA values of the same edge.
Checked by running the code in Verilator 5; the printed output supports the answer above. The assertion fails at t=15 and t=25 but not at t=5: it compares preponed samples, not the post-NBA values. The always block sees a one-cycle-delayed b, so b == a can only hold on the first edge.
Equating the Observed region (where the property is evaluated) with the sampling point is wrong: the sampling already happened in Preponed. Also, without the #1, the edge-25 failure shares its time slot with $finish and whether it is reported is tool-dependent.
How would you rewrite the property to compare b against the previous-cycle a using $past? Model answer: assert property (@(posedge clk) b == $past(a)); it passes on all three edges (b at an edge is a as sampled one edge earlier, and $past before the first tick returns the initial value 0).
Check the sampling first: concurrent assertions sample in Preponed, before the NBAs of the same edge. So at the first edge both a and b are still 0 and it passes, then it fails at the next two edges, because b is just a one-cycle-late copy of a. The trap is reading the post-NBA values, or thinking the Observed region is where the sampling happens. Next I would write the intended check with $past and put a short delay before $finish so the last edge is reported by every tool.