Difficulty: Medium · Puzzle 2 of 6 · Topic: Sequence Puzzles
Property intent: after start, observe two occurrences of a (not necessarily consecutive), then one cycle later done. Timeline: C20 start=1, C22 a=1, C24 a=1, C25 done=1. Determine the verdict.
property p_seq_goto;
@(posedge clk) start |-> ##1 a[->2] ##1 done;
endpropertyCompare [->2] behavior to [*2].
1) start triggers at C20; ##1 shifts matching window to C21 onward.
2) a[->2] consumes two a hits at C22 and C24, allowing gaps.
3) ##1 done then requires done at C25.
4) done is high at C25, satisfying consequent.Answer: PASS - [->2] allows non-consecutive matches, so hits at C22/C24 are legal and done arrives exactly one cycle later.
Interviewees frequently misread [->2] as consecutive repetition and incorrectly fail this waveform.
How would verdict change if the sequence used a[*2] instead of a[->2]?