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 its result disagrees with post-NBA intuition.
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 $error("[%0t OBSERVED] sampled mismatch: b != a", $time);
initial begin
repeat (3) @(posedge clk);
$finish;
end
endmoduleConcurrent assertions sample in preponed, not after NBAs.
1) At t=5, sampled values are a=0 and b=0, so assertion passes.
2) The always block then schedules a<=1 and b<=0 in NBA.
3) At t=15, sampled values are a=1 and b=0 from previous cycle state, so assertion fails.
4) At t=25, sampled values are a=0 and b=1, so it fails again.
5) Observed-region evaluation still uses preponed sampled data.Answer: Pass at t=5, fail at t=15 and t=25. The assertion compares preponed samples, so it effectively checks previous-cycle relationship, not same-edge post-NBA values.
Equating observed evaluation time with observed sampling time is wrong; sampling already happened earlier.
How would you rewrite the property to intentionally compare against previous-cycle a using $past?