Difficulty: Easy · Puzzle 6 of 6 · Topic: Implication Puzzles
Property intent: if either request source rises, grant must follow one cycle later. Timeline (all other samples are 0): req_a stays 0, req_b rises 0->1 at C40, and grant stays 0 at C41. Determine the verdict.
property p_or_antecedent;
@(posedge clk) ($rose(req_a) or $rose(req_b)) |-> ##1 grant;
endpropertyOnly one side of the OR needs to trigger the implication.
1) At C40, $rose(req_b) is true while $rose(req_a) is false.
2) OR antecedent is therefore true, so a checking thread is spawned.
3) ##1 grant requires grant at C41.
4) grant is low at C41, so the consequent fails and the property FAILS at C41.
5) A reader who thinks both sources must rise sees no trigger at all and reports a vacuous pass, which is the wrong verdict here.Answer: FAIL at C41 - one rising side is enough to launch the check, and grant is missing one cycle after the req_b rise.
Checked by running the code in Verilator 5; the printed output supports the answer above. One rising source is enough to start the check, and grant is missing at C41.
The wrong reading ('OR needs both rises') starts no attempt and reports a green vacuous pass, hiding a real missing grant. Because an OR antecedent fires when either side is true, the req_b rise alone creates the obligation.
What changes if grant is high at C41, and what if neither request rises? Model answer: with grant high at C41 the C40 attempt is a real (non-vacuous) PASS. If neither request rose, no attempt starts and the property reports a VACUOUS-PASS, which proves nothing about the grant path.
The antecedent is an or, so one rising source is enough. The rise of req_b at C40 starts the check, and grant must be high at C41. Grant is low at C41, so the property fails there. The trap is thinking both requests must rise, which starts no attempt and gives a green vacuous pass that hides a real missing grant. I would next add a cover on each side of the or.