goto [->N] & Non-Consecutive [=N] Repetition

Two operators for scattered occurrences

Consecutive repetition requires back-to-back ticks. Real traffic is rarely back-to-back: you want "the 3rd ack, whenever the acks happen to arrive". Both [->N] (goto) and [=N] (non-consecutive) count N possibly-scattered occurrences of a boolean, allowing any number of non-occurrence ticks between them. They differ in exactly one thing — where the sequence is allowed to end . Goto must end ON the tick of the Nth occurrence. Non-consecutive may extend past it through additional non-occurrence ticks before ending.

// goto: endpoint IS the Nth occurrence tick
sequence s_third_ack_goto;
  start ##1 ack [->3];        // ends exactly on the 3rd ack
endsequence

// non-consecutive: endpoint may drift past the Nth occurrence
sequence s_third_ack_eq;
  start ##1 ack [=3];         // 3 acks total, trailing gap allowed
endsequence

// Formal definitions from the LRM:
//   b [->N]  ===  (!b [*0:$] ##1 b) [*N]
//   b [=N]   ===  b [->N] ##1 !b [*0:$]

Side by side on the identical waveform

This is the #1 interview discriminator question for repetition. Same stimulus, both operators, followed by the same next element — watch where each one permits done to appear.

STIMULUS (identical for both operators)

clk   :  1    2    3    4    5    6    7    8    9
start :  0    1    0    0    0    0    0    0    0
ack   :  0    0    1    0    1    0    0    1    0
              A    a1        a2             a3
3rd ack occurs at tick 8.

CASE 1 — start ##1 ack[->3] ##1 done
clk   :  1    2    3    4    5    6    7    8    9
done  :  0    0    0    0    0    0    0    0    1
                                            E    M
E = ack[->3] endpoint LOCKED to tick 8 (the 3rd ack itself)
M = done required at exactly tick 9 → MATCH
If done instead came at tick 10 or 11: FAIL — no flexibility.

CASE 2 — start ##1 ack[=3] ##1 done
clk   :  1    2    3    4    5    6    7    8    9   10   11
ack   :  0    0    1    0    1    0    0    1    0    0    0
done  :  0    0    0    0    0    0    0    0    0    0    1
                                            e8   e9   e10  M
[=3] can end at tick 8, 9, 10, ... (trailing !ack gap allowed)
→ threads exist expecting done at 9, 10, 11, ...
done at tick 11 → the thread that ended [=3] at tick 10 MATCHES.
Same done at tick 11 under [->3]: FAIL. That is the whole difference.

One caveat hides in the trailing gap: the [=3] extension threads consume !ack ticks. If a 4th ack fires before done, threads that extended past it die — the gap must be occurrence-free, not merely idle time.

Endpoint alignment: why goto is the default

Because [->N] pins its endpoint to the Nth occurrence, whatever follows it is timed relative to that occurrence — which is almost always what a protocol means: "one cycle after the 4th beat, the burst response appears". [=N] deliberately un-anchors the endpoint, which is only what you want when the follow-on event has no timing relationship to the last occurrence — "3 retries happen, and sometime later the link gives up". When in doubt, write goto; reach for [=N] only when you can articulate why the trailing gap is part of the spec.

// PROTOCOL TIMING: response 1 cycle after the 4th beat → goto
property p_burst_resp;
  @(posedge clk) burst_start |-> beat_valid [->4] ##1 resp_valid;
endproperty
a_burst: assert property (p_burst_resp);

// LOOSE COUPLING: after 3 nacks, link_down eventually (window) → [=N]
property p_retry_giveup;
  @(posedge clk) $rose(txn_start) |-> nack [=3] ##1 link_down;
endproperty
a_retry: assert property (p_retry_giveup);

// Nth-occurrence grab with goto + sampled value:
property p_fourth_beat_last;
  @(posedge clk) burst_start |-> beat_valid [->4] ##0 beat_last;
endproperty  // the 4th beat itself must carry beat_last (##0 fusion)

ENDPOINT ALIGNMENT — beat_valid[->4] ##0 beat_last

clk        :  1    2    3    4    5    6    7
beat_valid :  0    1    1    0    1    1    0
beat_last  :  0    0    0    0    0    1    0
                   b1   b2        b3   b4
                                       EM
[->4] endpoint = tick 6 (4th beat). ##0 fuses beat_last check
onto that very tick → beat_last=1 @6 → MATCH.
With [=4] the endpoint could drift to tick 7+ where beat_valid=0,
and ##0 beat_last would test the WRONG cycle — a silent mis-check.

Interview angle and review

Interview angle

• "Draw a waveform where [->3] ##1 done fails but [=3] ##1 done passes." — done two or more cycles after the 3rd occurrence. If you can produce this on a whiteboard you have answered the real question.

• "Define [->N] in terms of primitive operators." — (!b[*0:$] ##1 b)[*N]; and [=N] is [->N] ##1 !b[*0:$]. Quoting the LRM expansions is a strong senior signal.

• "When would you actually use [=N]?" — counting events whose follow-up is not cycle-anchored to the last event (retry exhaustion, error thresholds). Default to goto otherwise.

• "What kills the trailing gap of [=N]?" — another occurrence of the counted boolean; the gap must be occurrence-free.

Key takeaways

• [->N] and [=N] both count N scattered occurrences; they differ only in endpoint freedom.

• [->N] ends exactly on the Nth occurrence — follow-on elements are timed off that event.

• [=N] permits a trailing occurrence-free gap — the follow-on is decoupled from the Nth event's cycle.

• Default to goto for protocol checks; use [=N] only when the trailing gap is genuinely part of the spec.

Common pitfalls

• Using [=N] where the spec times the next event off the Nth occurrence — the checker silently accepts late responses.

• Using [->N] for "N errors then eventually shutdown" — false failures when shutdown is not cycle-adjacent.

• Forgetting [=N] threads die if the counted event fires again during the trailing gap.

• Assuming [->N] requires consecutive occurrences — gaps between occurrences are fine; only the endpoint is pinned.

• Standalone b[=N] as a full property — its drifting endpoint makes pass times meaningless; anchor it to something.