Difficulty: Hard · Puzzle 5 of 6 · Topic: Implication Puzzles
Property intent: after req, busy must stay high throughout the wait-until-rsp window (rsp expected 1 to 3 cycles later). Timeline: 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.
1) req at C30 launches consequent.
2) rsp is matched at C32 via ##2 path in ##[1:3].
3) busy must hold throughout that chosen window.
4) busy is 0 at C32, violating throughout.Answer: FAIL - rsp arrives in-range, but busy is not maintained for the full matched window, breaking throughout.
People often treat throughout like an endpoint check instead of a per-cycle obligation over the sequence interval.
If rsp moved to C31 with busy still 1 at C31, would this become a pass?