Difficulty: Hard · Puzzle 3 of 6 · Topic: Sequence Puzzles
Property intent: after start, match two nonconsecutive a occurrences, then done one cycle after the match ends. Timeline (all other samples are 0, so a=0 at C30, C32, C34 and later): C30 start=1, C31 a=1, C33 a=1, C35 done=1. Determine the verdict, and say what a[->2] would do with the same waveform.
property p_seq_nonconsecutive;
@(posedge clk) start |-> a[=2] ##1 done;
endproperty[=2] is goto repetition plus any number of trailing cycles where a stays low. List every cycle where the match can end.
1) start triggers at C30. a[=2] counts the two a samples at C31 and C33.
2) Unlike [->2], a[=2] may keep matching after the second a for as long as a stays low, so its legal end points are C33, C34 and C35 (until the next a).
3) ##1 done needs done one cycle after one of those end points. Taking the end at C34, done must be at C35, and it is.
4) So the sequence matches and the property passes. With a[->2] the only end point is C33, done would be needed at C34, and the same waveform would FAIL.
5) Tool note: some free tools (for example Verilator 5.048) reject [=n] followed by ##; reason with end points or use a full SVA simulator.Answer: PASS - the two a matches occur, and done is observed one cycle after the legal end point C34 of the [=2] match (a[->2] would FAIL here).
Checked by running a model of the rule in Verilator 5 and a Python model. Verilator runs a[->2] spelled out as a gap-tolerant pair of hits: it ends on the second a (C33), so done is needed at C34 and the check fails. A small model of the LRM end-point semantics (it also reproduces the Verilator verdicts above): [=2] has several legal end points, so it passes where [->2] fails.
[=n] is [->n] plus a tail of non-a cycles, so its end point is flexible while [->n] ends exactly on the n-th a. This waveform is passed by [=2] and failed by [->2], which is why done at C35 is legal here.
Would adding an extra a pulse at C34 still pass? Model answer: No, it FAILS. With a high at C34 the tail of low cycles stops at C33, so the only legal end of a[=2] is C33, ##1 done requires done at C34, and done is at C35. (A third a before the second match ends, for example a also high at C30, also breaks the exactly-two count.)
I would list the a hits at C31 and C33, then done at C35. With the nonconsecutive repetition the match can end at C33, C34 or C35 while a stays low, so the end at C34 followed by done at C35 is legal and the property passes. The goto form ends only on the second a, so it would need done at C34 and would fail on this same waveform. The trap is treating the two operators as the same; I would check which end point the spec really means.