Difficulty: Medium · Puzzle 3 of 6 · Topic: Assertion Debug Puzzles
Property intent: functional req must get gnt in up to 2 cycles. Timeline: req pulses at C60 and C66, but scan_mode=1 on both cycles; gnt never asserts. Determine the verdict.
property p_mode_gated_req;
@(posedge clk) (req && !scan_mode) |-> ##[0:2] gnt;
endpropertyCheck whether antecedent is ever true in sampled cycles.
1) req is present, but scan_mode=1 each time req is high.
2) Antecedent req && !scan_mode is never true.
3) No checking thread is spawned.Answer: VACUOUS-PASS - all req pulses are masked out of the antecedent, so no functional grant obligation is actually checked.
Teams may celebrate green assertions while completely missing functional traffic due to over-gated antecedents.
What extra assertion or cover would you add to guarantee non-scan req activity is exercised?