Difficulty: Hard · Puzzle 5 of 6 · Topic: Implication Puzzles
Property intent: after req, busy must stay high until rsp arrives (rsp expected 1 to 3 cycles later). Timeline (all other samples are 0): C30 req=1 busy=1, C31 busy=1, C32 busy=0 rsp=1. Determine the verdict.
property p_hold_until_rsp;
@(posedge clk) req |-> busy throughout (##[1:3] rsp);
endpropertythroughout requires the boolean expression on every cycle used by the matched sequence, including the last one.
1) req at C30 launches consequent.
2) rsp is matched at C32 via the ##2 path in ##[1:3].
3) busy must hold on every cycle of that matched window, C30 through C32, and the last cycle counts.
4) busy is 0 at C32, violating throughout. Note this means busy dropping in the same cycle as rsp is a FAIL, even though that is a natural handshake; if the intent allows it, the property must say so.Answer: FAIL - rsp arrives in-range, but busy is not maintained for the full matched window including the rsp cycle, breaking throughout (reported at C32).
Checked by running the code in Verilator 5; the printed output supports the answer above. busy drops in the same cycle as rsp (C32), and throughout covers that last cycle, so it fails.
People often treat throughout like an endpoint check instead of a per-cycle obligation over the sequence interval, and the interval includes the cycle where rsp is seen. The phrase 'busy stays high until rsp' invites reading it as 'busy may fall with rsp'; the code does not.
If rsp moved to C31 with busy still 1 at C31, would this become a pass? Model answer: PASS. rsp matches via ##1 at C31 and busy is high at C30 and C31, so throughout holds; busy dropping at C32 is outside the matched window and is not checked.
I would find the rsp match first: it arrives at C32, inside the one to three range. Throughout then requires busy on every cycle of the matched window, C30 through C32, including the rsp cycle. Busy is low at C32, so the property fails at C32. The trap is reading busy stays high until rsp as busy may fall with rsp; the code does not allow that, so I would ask whether the intent needs the window to stop one cycle earlier.