Difficulty: Medium · Puzzle 1 of 6 · Topic: Assertion Debug Puzzles
Property intent: after req, gnt must arrive 1 to 3 cycles later, except while reset is active. The DUT loses the request when a one-cycle reset glitch hits, and gnt never arrives. Timeline (all other samples are 0 except rst_n): C50 req=1 rst_n=1, C51 rst_n=0, C52 rst_n=1 and stays 1, gnt=0 throughout. What do p_disable and p_plain (the same property without disable iff) report for the C50 attempt?
property p_disable;
@(posedge clk) disable iff (!rst_n) req |-> ##[1:3] gnt;
endproperty
property p_plain;
@(posedge clk) req |-> ##[1:3] gnt;
endpropertyCheck what happens to in-flight attempts when the disable iff condition becomes true, and what the log shows afterwards.
1) req at C50 starts an attempt with window C51..C53 in both properties.
2) rst_n is sampled low at C51. In p_disable that makes the disable condition true, so the in-flight attempt is discarded: it is neither a pass nor a fail, and it is not vacuous either (the antecedent was true).
3) rst_n returns to 1 at C52, but the discarded attempt does not come back, so the missing gnt is never examined.
4) p_plain has no abort: the attempt runs to the end of its window and FAILS at C53 because gnt never came.Answer: p_disable: no failure is reported (the attempt is aborted at C51); p_plain: FAIL at C53. A one-cycle reset glitch silently hides a real lost-grant bug.
Checked by running the code in Verilator 5; the printed output supports the answer above. The one-cycle reset glitch aborts the disable-iff attempt silently; the plain property reports the lost grant at C53.
An aborted attempt is not a 'vacuous pass'; vacuous means the antecedent was false. Here the antecedent fired and the check was thrown away, and the log is green. Debug sessions that treat the quiet property as proof of a good grant path miss the bug.
How would you make a mid-transaction reset visible instead of silently masked? Model answer: keep disable iff for the protocol check but add (1) an assertion without disable iff that the DUT really cleared its state on reset, (2) a cover such as req ##[1:3] !rst_n so aborted attempts are counted in regressions, and (3) if reset during a transaction is illegal, assert on it directly or use reject_on(!rst_n) (where the tool supports it) so the abort becomes an explicit failure.
I would trace the attempt from C50 with its window C51 to C53. In the version with disable iff, reset is low at C51, so the attempt is discarded; it is not a pass, not a fail and not vacuous, and it does not come back at C52. So it reports nothing. The plain version runs to the end of the window and fails at C53. The trap is trusting the green log; a one cycle reset glitch hides a lost grant. I would check why reset glitched and cover reset during pending requests.