Difficulty: Hard · Puzzle 3 of 6 · Topic: Sequence Puzzles
Property intent: after start, match two nonconsecutive a occurrences, then one cycle later done. Timeline: C30 start=1, C31 a=1, C33 a=1, C34 a=0, C35 done=1. Determine the verdict.
property p_seq_nonconsecutive;
@(posedge clk) start |-> a[=2] ##1 done;
endpropertyRecall that [=n] is nonconsecutive repetition and is not the same as [*n].
1) start triggers at C30.
2) a[=2] finds two a matches at C31 and C33 with a legal gap at C32.
3) The sequence can still complete before checking done.
4) done at C35 satisfies ##1 from the chosen sequence end.Answer: PASS - the two required nonconsecutive a matches occur, and done is observed one cycle after a legal end point of the [=2] match.
People often conflate [=n] with [->n]; the end-point flexibility differs and changes timing outcomes.
Would adding an extra a pulse at C34 necessarily invalidate this match? Explain match-end selection.