Difficulty: Easy · Puzzle 2 of 6 · Topic: Implication Puzzles
Property intent: every req must be granted within 0 to 2 cycles. In this test, req never becomes 1. Determine the verdict.
property p_vacuous;
@(posedge clk) req |-> ##[0:2] gnt;
endpropertyAsk whether the antecedent ever spawns a checking thread.
1) req is never true at a sampled clock edge.
2) No implication attempts are triggered.
3) With no triggered antecedent, implication succeeds vacuously.Answer: VACUOUS-PASS - antecedent never triggers, so no failing obligation is created.
Vacuous pass is logically valid but dangerous if used as evidence of functional correctness without coverage.
What companion cover/assert would you add to ensure this property is meaningfully exercised?