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 (all other samples are 0): 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, and ends exactly on the second hit (C24).
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 after the second hit.
Checked by running the code in Verilator 5; the printed output supports the answer above. Goto [->2] accepts the gap between the two a hits and passes; consecutive a[*2] on the same trace fails.
Interviewees frequently misread [->2] as consecutive repetition and incorrectly fail this waveform. The other trap is the end point: goto ends on the last a, so ##1 done is counted from C24, not from the cycle after the last low cycle.
How would the verdict change if the sequence used a[*2] instead of a[->2]? Model answer: it would FAIL. After ##1 the repetition a[*2] needs a high at C21 and C22, but a is 0 at C21, and the hits at C22 and C24 are not adjacent. Only [->n] (and [=n]) tolerate the gaps.
I would mark the a hits at C22 and C24, and done at C25. Goto repetition allows gaps between the hits and ends exactly on the second one, C24. So done one cycle later at C25 is exactly what the property wants, and it passes. The trap is misreading the goto as consecutive and failing it; I would next ask what happens if done comes later, because goto ends on the last a.