Difficulty: Medium · Puzzle 1 of 6 · Topic: Sequence Puzzles
Property intent: after req, gnt must arrive exactly 2 cycles later, then busy must stay high for 2 to 3 consecutive cycles. Timeline (all other samples are 0): C10 req=1, C12 gnt=1, C13 busy=1, C14 busy=0, C15 busy=1. Determine the verdict for the C10 attempt.
property p_seq_range;
@(posedge clk) req |-> ##2 gnt ##1 busy[*2:3];
endpropertyCheck consecutive repetition semantics of [*2:3]. Count busy highs, then count how many are adjacent.
1) Antecedent req triggers at C10.
2) ##2 gnt requires gnt at C12, which is satisfied.
3) busy[*2:3] starts at C13 and needs two adjacent high samples (C13 and C14) before it may stop, or three (C13, C14, C15).
4) busy is high at C13 but low at C14, so the run is only one cycle long and the minimum of 2 is not reached. The later high at C15 does not repair it: [*n] never skips cycles.
5) The attempt fails when the C14 sample is taken.Answer: FAIL - the attempt from C10 fails at C14: grant timing is correct, but busy has only a one-cycle run (C13), so [*2:3] never reaches its minimum of 2 consecutive cycles.
Checked by running the code in Verilator 5; the printed output supports the answer above. The C10 attempt fails at C14: busy is high only one cycle in a row, so [*2:3] never reaches 2.
The waveform has busy high at C13 and again at C15, so a reading of [*2:3] as 'busy is seen high two or three times' passes it. [*2:3] is consecutive: the C14 low cycle ends the run after one cycle and the C15 high starts a new run that is too late.
If busy were high at C13 and C14 and low at C15, would the same property pass or fail? Model answer: PASS. busy[*2:3] matches the two-cycle run C13..C14 and the match ends at C14. Nothing in the property requires a third high cycle, and the three-cycle alternative simply does not match, which is allowed because [*2:3] is a range.
I would first mark busy per cycle: high at C13, low at C14, high at C15. The grant at C12 is exactly two cycles after req, so that part is fine, but busy[*2:3] needs two consecutive highs starting at C13. The property fails at C14, because the run is only one cycle long and the later high at C15 cannot repair it. The trap is reading the repetition as busy being seen high two or three times; I would next check whether the intent really was consecutive.