Difficulty: Hard · Puzzle 6 of 6 · Topic: Verifying CDC & Reset Puzzles
Domain B must not leave reset before domain A. Two candidate assertions: p1 is $rose(rstB_n) |-> rstA_n and p2 is $rose(rstB_n) |-> $past(rstA_n). In this run both resets are released by the same edge (t=15, non-blocking). Which assertion fails, at what time, and what does each one actually require?
`timescale 1ns/1ns
module tb;
bit clk = 0;
always #5 clk = ~clk; // posedges at 5, 15, 25, 35
bit rstA_n = 0, rstB_n = 0;
int cyc = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 1) begin rstA_n <= 1; rstB_n <= 1; end // both released by the edge at t=15
end
p1: assert property (@(posedge clk) $rose(rstB_n) |-> rstA_n)
else $display("p1 FAIL at %0d", $time);
p2: assert property (@(posedge clk) $rose(rstB_n) |-> $past(rstA_n))
else $display("p2 FAIL at %0d", $time);
always @(posedge clk) if ($rose(rstB_n)) $display("t=%0d rstB_n rose in the sampled values", $time);
initial begin
#36 $finish;
end
endmoduleConcurrent assertions use values sampled just before the clock edge.
1) Both resets are released by non-blocking assignments at the edge at t=15, so their sampled values change at the edge at t=25.
2) At t=25 the sampled rstB_n is 1 and its previous sample (t=15) was 0: $rose(rstB_n) is true at t=25.
3) p1 checks the sampled rstA_n at that same edge: it is 1, so p1 passes. p1 therefore allows B to leave reset on the same edge as A.
4) p2 checks $past(rstA_n), the value one clock earlier (sampled at t=15): 0, so p2 fails at t=25. p2 requires A to have been released at least one full cycle before B.
5) So 'B must not leave reset before A' is p1; 'B must leave strictly after A' is p2. Choose by the specification: if the release is meant to be simultaneous, p2 would give a false failure.Answer: p2 fails at t=25 and p1 passes (the print shows $rose(rstB_n) at t=25). p1 means 'A is already released when B is' (same edge allowed); p2 means 'A was released at least one cycle earlier'. State which the spec asks for.
Checked by running the code in Verilator 5; the printed output supports the answer above. Verilator 5 with --assert: p2 fails at t=25; p1 never fails.
Reading $rose and rstA_n as if both were the post-edge values. Assertions use the preponed samples, so a release by a non-blocking assignment at an edge appears at the next edge, and the same-cycle release of two signals is visible as 'both changed together' in p1.
How would you require A to be released strictly earlier but within at most 8 cycles of B's release? Model answer: $rose(rstA_n) |-> ##[1:8] $rose(rstB_n), which demands B's release between 1 and 8 cycles after A's; p2 can stay as the ordering check.