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 (all samples 0). 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.
Checked by running the code in Verilator 5; the printed output supports the answer above. With req never high the property never fails and the antecedent cover never hits: the pass is vacuous.
Vacuous pass is logically valid but dangerous if used as evidence of functional correctness without coverage. Some tools count it as a pass in the summary; look for the vacuous or non-vacuous split.
What companion cover/assert would you add to ensure this property is meaningfully exercised? Model answer: a cover property on the antecedent (cover property (@(posedge clk) req)) to prove the trigger happens, and ideally cover property (req ##[0:2] gnt) to prove a real non-vacuous pass; a regression with zero hits on either is a hole.
With req never high, the antecedent never triggers, so no attempt is ever created and the property passes vacuously. That is logically valid but it proves nothing about grants. The trap is counting that green result as evidence of correctness. I would next look at the vacuous versus non-vacuous split, and add a cover on the antecedent so I know the test really sent a request.