Difficulty: Medium · Puzzle 4 of 6 · Topic: Assertion Debug Puzzles
Property intent: every req must get its own gnt within 1 to 3 cycles. Timeline (all other samples are 0): C10 req=1, C11 req=1, C12 gnt=1 (a single grant pulse, and no other grants). Determine the verdict, and say whether the green log proves both requests were granted.
property p_bounded_resp;
@(posedge clk) req |-> ##[1:3] gnt;
endpropertyEach req starts its own attempt. Write down the window of each attempt and check whether the single gnt falls inside both.
1) The req at C10 starts attempt A with window C11..C13; the req at C11 starts attempt B with window C12..C14.
2) gnt at C12 lies inside both windows, so attempt A and attempt B each find a match.
3) No failure is reported even though one gnt pulse served two requests.
4) The property is per attempt and has no notion of one-to-one matching, so a lost grant is invisible.Answer: PASS (no failure) - the single gnt at C12 satisfies both overlapping attempts, so the green log does not prove two grants were issued.
Checked by running the code in Verilator 5; the printed output supports the answer above. No failure is reported although 2 requests were answered by 1 grant pulse: the green log does not prove two grants.
A bounded-response assertion checks each attempt independently. Back-to-back requests make attempts overlap, and one late or shared grant can satisfy several of them. (With the lone grant at C14 instead, attempt A fails at C13 while B passes, so only the earliest request is flagged.)
What extra check catches the lost grant? Model answer: add a one-to-one check, typically a scoreboard counter: increment on req, decrement on gnt, assert it never goes negative and returns to zero within the maximum latency after the last req. For in-order protocols a queue of request timestamps checked at each gnt does the same job. Keep the bounded-response assertion for latency.
I would draw the two windows: the request at C10 allows a grant at C11 to C13, the request at C11 allows C12 to C14. The single grant at C12 falls in both, so each attempt finds a match and the property passes. The trap is believing the green log proves two grants; the property has no one to one matching, so a lost grant is invisible. I would add a scoreboard or a count check that requests and grants match.