Difficulty: Medium · Puzzle 5 of 6 · Topic: Assertion Debug Puzzles
Property intent: after en turns on, loaded must be high one cycle later; checks are off during reset. The DUT ignores en while in reset and never loads. Timeline (all other samples are 0): rst_n=0 at C80..C83 and 1 from C84; en rises 0->1 at C81 and stays 1 afterwards; loaded=0 throughout. What do p_en and p_en_fix report?
property p_en;
@(posedge clk) disable iff (!rst_n)
$rose(en) |=> loaded;
endproperty
property p_en_fix;
@(posedge clk) disable iff (!rst_n)
($rose(en) || (en && $rose(rst_n))) |=> loaded;
endpropertyFind the only edge where $rose(en) is true and check whether reset is active there. Then ask whether it can be true again after reset release.
1) $rose(en) is true only at C81 (0 at C80, 1 at C81). At every later edge en was already 1, so it is false.
2) rst_n is 0 at C81, so disable iff discards that attempt. It is not a pass or a fail.
3) At C84 reset is released but en was 1 at C83 and is 1 at C84, so $rose(en) is false: no attempt ever starts after reset. p_en reports nothing for the whole run although loaded never goes high.
4) p_en_fix adds en && $rose(rst_n), true at C84, so an attempt starts there and loaded is required at C85. It is 0, so p_en_fix FAILS at C85.Answer: p_en: no failure (the only $rose(en) lands inside reset and is discarded, none follows); p_en_fix: FAIL at C85.
Checked by running the code in Verilator 5; the printed output supports the answer above. The only $rose(en) falls inside reset and is discarded, so p_en stays silent; p_en_fix also starts at reset release and fails at C85.
The event the assertion waits for happened while reset masked it, and an edge detector never re-arms while the signal just stays high. The log is green because no attempt exists at all, not because loaded was checked. If an enable can be held across reset release, trigger on its level at release too.
How would you catch this class of bug without relying on the edge? Model answer: assert the state after reset release, for example (rst_n && $past(!rst_n) && en) |=> loaded, or check the loaded state in a scoreboard, and add a cover on $rose(en) with rst_n high so regressions prove the edge is exercised outside reset.
I would find the only rose of en: it is at C81, inside reset, so the attempt is discarded. At C84 reset is released but en was already high, so there is no rose and no attempt ever starts. The plain property reports nothing even though loaded never goes high. The fixed version also triggers on en together with the rise of reset, so it starts at C84 and fails at C85. The trap is an edge detector that never re-arms when the signal just stays high. I would trigger on the level at reset release.