Difficulty: Medium · Puzzle 1 of 6 · Topic: Assertion Debug Puzzles
Property intent: after req, gnt must arrive within 1 to 2 cycles, except when reset is active. Timeline: C50 req=1 and rst_n=1, C51 rst_n=0, C52 rst_n=0 gnt=0, C53 rst_n=1. Determine the verdict for the C50 attempt.
property p_disable_abort;
@(posedge clk) disable iff (!rst_n) req |-> ##[1:2] gnt;
endpropertyCheck what happens to in-flight threads when disable iff becomes true.
1) req at C50 starts a checking thread.
2) rst_n goes low at C51, making disable iff condition true.
3) Active thread is aborted (discarded) immediately.
4) Aborted thread does not report fail for missing gnt.Answer: VACUOUS-PASS - the in-flight obligation is aborted by disable iff, so no failure is reported for that attempt.
Debug sessions often misclassify aborted threads as hidden fails, leading to wrong RTL fixes.
What property pattern would you use if reset should cause an explicit failure instead of abort?