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 cycles. Timeline: C10 req=1, C12 gnt=1, C13 busy=1, C14 busy=0. Determine the verdict.
property p_seq_range;
@(posedge clk) req |-> ##2 gnt ##1 busy[*2:3];
endpropertyCheck consecutive repetition semantics of [*2:3].
1) Antecedent req triggers at C10.
2) Consequent requires gnt at C12, which is satisfied.
3) Then busy[*2:3] starts at C13 and needs at least C13 and C14 high.
4) busy drops at C14, so only one high cycle is seen.Answer: FAIL - grant timing is correct, but busy does not satisfy the minimum 2-cycle consecutive hold required by [*2:3].
Many candidates correctly check ##2 but forget that [*2:3] is consecutive repetition, not two observations with gaps.
If busy were high at C13 and C14 and dropped at C15, would the same property pass or fail?