Difficulty: Medium · Puzzle 4 of 6 · Topic: Implication Puzzles
Property intent: after req, grant may arrive in the next cycle or one cycle later in the consequent window. Timeline: C20 req=1, C21 gnt=1, C22 gnt=0. Determine the verdict.
property p_nonoverlap_range;
@(posedge clk) req |=> ##[0:1] gnt;
endpropertyBecause of |=>, the ##[0:1] window starts one cycle after req.
1) req at C20 triggers non-overlapped consequent starting at C21.
2) ##[0:1] allows gnt at C21 or C22.
3) gnt is high at C21, satisfying the earliest legal point.Answer: PASS - with |=>, the search window is C21 to C22, and gnt is present at C21.
A frequent error is adding one extra cycle twice (once for |=> and again mentally for ## range).
Would the same waveform pass or fail if the operator were |-> instead of |=>?