Difficulty: Medium · Puzzle 4 of 6 · Topic: Implication Puzzles
Property intent: after req, grant may arrive in the next cycle or one cycle after that (the window is counted after the |=> shift). Timeline (all other samples are 0): C20 req=1, C21 gnt=0, C22 gnt=1. Determine the verdict.
property p_nonoverlap_range;
@(posedge clk) req |=> ##[0:1] gnt;
endpropertyBecause of |=>, the ##[0:1] window starts one cycle after req, so it ends one cycle later than you may expect.
1) req at C20 triggers non-overlapped consequent starting at C21.
2) ##[0:1] allows gnt at C21 or C22.
3) gnt is low at C21 but high at C22, the last legal cycle, so the consequent matches.
4) With |-> instead the window would be C20..C21 and this grant would be too late.Answer: PASS - with |=>, the search window is C21 to C22, and gnt arrives at C22, the last legal cycle.
Checked by running the code in Verilator 5; the printed output supports the answer above. |=> shifts the window to C21..C22 so gnt at C22 passes; the same range after |-> would be C20..C21 and fail.
The grant is on the very last legal cycle. Forgetting the |=> shift gives window C20..C21 and a false FAIL; double-counting the shift gives C23 and lets a late grant slip through. The waveform has gnt only at C22 so that exactly one of those readings fails.
Would the same waveform pass or fail if the operator were |-> instead of |=>? Model answer: FAIL, reported at C21. |-> ##[0:1] gnt looks at C20 and C21, and gnt is low at both; the C22 grant is outside the window. (If gnt were high at C21, both operators would pass, which is why this waveform uses C22.)
With the non-overlapped arrow the search starts one cycle after req, so the window is C21 to C22. Gnt is low at C21 and high at C22, the last legal cycle, so the property passes. The trap is forgetting the shift, which gives C20 to C21 and a false failure, or counting the shift twice and letting a late grant through. I would check the boundary by moving the grant to C23 and confirming it fails.