Repetition Operators

Module 12 · Page 12.9

Three Operators, Three Spec Rules

Module 12.5 introduced the ## delay operators that glue boolean conditions across cycles into sequences. Module 12.8 covered implication, the contract layer that gates a consequent on an antecedent. This page covers the third structural piece of the temporal vocabulary: repetition operators — the syntactic mechanisms for expressing "this happens N times in a row," "this happens N times eventually," and "the Nth occurrence is followed by something."

SVA provides three repetition operators. They look almost identical and produce contracts whose semantics differ in subtle but consequential ways:

• [*n] consecutive repetition — the boolean is true for N consecutive sampling events
• [=n] non-consecutive repetition — the boolean is true at N (not necessarily consecutive) sampling events
• [->n] goto repetition — the boolean is true at N events, and the Nth event is the chain's anchor point

These three encode three structurally different spec rules — burst protocols ("data valid for 4 consecutive cycles"), retry counters ("N error responses within a window"), and acknowledgment-with-followup ("after the Nth retry, the recovery sequence must complete").

Consecutive Repetition — [*n]

The [*n] operator matches when the boolean expression holds for N consecutive sampling events. It is the most common repetition form because most spec rules about duration are consecutive.

// ── Fixed count: signal must be high for exactly N consecutive cycles ──
sequence s_valid_4_cycles;
    valid [*4];
    // Equivalent to: valid ##1 valid ##1 valid ##1 valid
    // High for exactly 4 consecutive sampling events.
endsequence
 
// ── Range count: signal must be high for between m and n consecutive cycles ──
sequence s_valid_2_to_8_cycles;
    valid [*2:8];
    // High for any duration between 2 and 8 consecutive sampling events.
    // Matches if held for 2, 3, 4, 5, 6, 7, or 8 cycles.
endsequence
 
// ── Unbounded count: held for at least m consecutive cycles ──
sequence s_valid_at_least_3;
    valid [*3:$];
    // High for 3 or more consecutive cycles (no upper bound).
endsequence
 
// ── In a complete property — burst transfer ──────────────────────
property p_burst_transfer;
    @(posedge clk) disable iff (rst)
        $rose(start) |-> data_valid [*4] ##1 burst_done;
    // After start rises, data_valid must be high for 4 consecutive cycles,
    // then burst_done in the cycle after.
endproperty

The semantic rule. [*n] matches when every one of N consecutive sampling events sees the boolean as true. A single low-cycle in the middle resets the count — the operator does not match "4 cycles total, gaps allowed." For that, use [=n].

The range form [*m:n] matches any duration in the range, inclusive on both ends. [*0] is legal and represents a length-zero match (the boolean is checked zero times — a vacuous match). [*0:0] is the empty match; [*$] is unbounded.

Non-Consecutive Repetition — [=n]

The [=n] operator matches when the boolean is true at N events anywhere within a window. The events don't have to be consecutive — they just have to total N occurrences before the matching sequence ends.

// ── Fixed count: error fires exactly 3 times somewhere in this window ──
sequence s_three_errors;
    err_pulse [=3];
    // The sequence matches when err_pulse has fired 3 times.
    // The 3 firings can be in any cycles — not required to be consecutive.
endsequence
 
// ── In a property — retry-count protocol ──────────────────────────
property p_three_retries_then_fail;
    @(posedge clk) disable iff (rst)
        $rose(start) |-> err_pulse [=3] ##1 fatal_fail;
    // After start, if err_pulse fires 3 times (not necessarily in a row),
    // fatal_fail must follow.
endproperty
 
// ── Range: between m and n total occurrences ──────────────────────
sequence s_two_to_five_attempts;
    retry [=2:5];
endsequence

The semantic rule. [=n] is the count form: the boolean must be true at N events overall, but the cycles between those events can be anything (the boolean can be false). This matches "count of N retries within this window" or "the error has been observed 5 times" spec rules.

The match-extent rule. A sequence ending in [=n] matches at every cycle starting from the Nth occurrence onward, until the boolean fires again (which restarts the count for any subsequent match). Module 12.5's first_match is often paired with [=n] to capture only the earliest match.

Goto Repetition — [->n]

The [->n] operator is like [=n] — N events anywhere — with one critical difference: the matching sequence ends exactly at the Nth occurrence, not at any later cycle. This makes the Nth occurrence an anchor point for the next sequence step.

// ── Fixed count: anchor on the Nth occurrence ─────────────────────
sequence s_after_third_retry;
    retry [->3];
    // Matches exactly at the cycle of the 3rd retry occurrence.
    // The sequence ends ON that cycle (not at any later one).
endsequence
 
// ── In a property — recovery follows the Nth retry ──────────────
property p_recovery_after_third_retry;
    @(posedge clk) disable iff (rst)
        $rose(start) |-> retry [->3] ##1 recovery_start;
    // After start, on the cycle of the 3rd retry, the next cycle
    // must see recovery_start high.
endproperty
 
// ── Range: anchor on any occurrence in the m-to-n range ──────────
sequence s_between_2_and_5_retries;
    retry [->2:5];
endsequence

The semantic rule. [->n] is the goto form: like [=n], the boolean must be true at N events anywhere in the window. But [->n] ends the matching sequence at the cycle of the Nth occurrence, making that cycle the chain's anchor. The next sequence step (after ##1 or whatever) starts from there.

The semantic difference between [=n] and [->n] is which cycle the matching sequence ends on. [=n] lets the match extend until the next firing of the boolean; [->n] ends precisely at the Nth firing. For chained patterns where the next event must follow the Nth occurrence specifically, [->n] is the right tool.

Range Forms — [*m:n], [=m:n], [->m:n]

All three operators have range variants that match anywhere in the given count range.

// ── Burst-length range ──────────────────────────────────────────
property p_burst_length_in_window;
    @(posedge clk) disable iff (rst)
        $rose(burst_start) |->
            data_valid [*4:16] ##0 burst_done;
    // Burst length must be between 4 and 16 consecutive cycles.
endproperty
 
// ── Retry-count range ──────────────────────────────────────────
property p_retry_count_acceptable;
    @(posedge clk) disable iff (rst)
        $rose(start) |->
            err_pulse [=1:5] ##1 recovery_clean;
    // Between 1 and 5 errors must occur before clean recovery.
endproperty
 
// ── Goto range for "any retry from N to M triggers escalation" ──
property p_escalation_on_retry_range;
    @(posedge clk) disable iff (rst)
        $rose(start) |->
            retry [->3:5] ##1 escalation;
    // On the 3rd, 4th, or 5th retry (whichever happens first),
    // escalation must follow the next cycle.
endproperty

The unbounded form [*m:$] matches m or more consecutive (or non-consecutive, for [=m:$]) occurrences. Useful for "at least N cycles" or "at least N occurrences" rules without an upper bound. Production discipline usually pairs unbounded repetition with a separate hard-deadline assertion — the unbounded form alone doesn't enforce a bound, so it can vacuously pass on degenerate cases.

A Complete Working Example — Burst-Protocol Repetition Library

The pattern below shows production discipline: a property package encoding the repetition contracts for an AXI-style burst protocol. Each property uses the repetition operator that matches the spec rule's exact wording.

package burst_repetition_rules;
    default clocking @(posedge clk); endclocking
    default disable iff (!rst_n);
 
    // ── Rule 1 (spec §6.2): "data_valid must hold for 4 to 16 consecutive cycles during a burst"
    // Operator: [*m:n] consecutive range
    property p_burst_length(input bit burst_start, data_valid, burst_done);
        $rose(burst_start) |-> data_valid [*4:16] ##0 burst_done;
    endproperty
 
    // ── Rule 2 (spec §7.1): "between 1 and 3 error pulses are acceptable within a transaction"
    // Operator: [=m:n] non-consecutive range
    property p_error_count_acceptable(
        input bit txn_start, err_pulse, txn_complete
    );
        $rose(txn_start) |-> err_pulse [=1:3] ##1 txn_complete;
    endproperty
 
    // ── Rule 3 (spec §8.4): "escalation must follow exactly the 3rd retry"
    // Operator: [->n] goto, anchored on the 3rd occurrence
    property p_escalation_on_third_retry(
        input bit txn_start, retry, escalation
    );
        $rose(txn_start) |-> retry [->3] ##1 escalation;
    endproperty
 
    // ── Rule 4 (spec §9.2): "ready must be held high for at least 1 cycle until ack is sampled"
    // Operator: [*1:$] unbounded consecutive
    property p_ready_held_until_ack(input bit ready, ack);
        $rose(ready) |-> ready [*1:$] ##0 ack;
    endproperty
endpackage

What this code does. Four named properties, each encoding one burst-protocol spec rule. The operator choice for each property matches the spec rule's exact wording — consecutive duration → [*m:n], count-based retry threshold → [=m:n], goto-anchor escalation → [->n], unbounded hold → [*1:$]. A reviewer reading the property file with the spec open can verify each operator one row at a time.

Expected output (fragment from a regression).

# *E,ASRTST: [142] p_burst_length failed at 142ns
#   Burst length out of range: data_valid held for only 3 cycles
#
# Coverage summary:
#   c_burst_length_antecedent:           87 hits  (burst_start exercised)
#   c_error_count_antecedent:           187 hits  (txn_start exercised)
#   c_escalation_on_third_retry:         12 hits  (retry-counter scenarios)
#
# Total assertion failures: 1

The repetition-based assertions surface real spec violations with specific count and timing context. The cover properties confirm each antecedent fired in the regression — the assertion-cover pairing pattern from Module 12.6 working in concert with the repetition operators.

Common Pitfalls

Pitfall 1 — Consecutive vs non-consecutive confusion

// Intent: error has fired 3 times within this transaction
// Wrong:
property p_wrong;
    txn_start |-> err [*3];      // requires 3 CONSECUTIVE error cycles
endproperty
 
// Right:
property p_right;
    txn_start |-> err [=3];      // requires 3 errors anywhere in the window
endproperty

Fix: [*n] requires N consecutive cycles; [=n] requires N occurrences in any cycles. Pick the operator that matches the spec's exact wording — "N consecutive" vs "N total" is the structural distinction.

Pitfall 2 — [=n] vs [->n] confusion in chained patterns

// Intent: on the 3rd retry, the next cycle must see escalation
// Wrong:
property p_wrong;
    txn_start |-> retry [=3] ##1 escalation;
endproperty
 
// Right:
property p_right;
    txn_start |-> retry [->3] ##1 escalation;
endproperty

Fix: [=n] lets the matching sequence extend after the Nth occurrence; [->n] anchors precisely at the Nth occurrence. For chained patterns where the next event must follow the Nth occurrence specifically, use [->n]. The simulation behaviour of the two operators can differ by many cycles — the [=n] form allows escalation to match at any cycle after the 3rd retry; [->n] requires it on exactly the cycle after the 3rd retry.

Pitfall 3 — Unbounded repetition without a hard-deadline backup

// Intent: data_valid must eventually be high
property p_eventually_valid;
    $rose(start) |-> data_valid [*1:$];
    // Vacuously passes if the simulation ends without data_valid going high.
endproperty

Fix: unbounded repetition doesn't enforce a deadline. Pair with a hard-deadline assertion: assert property ($rose(start) |-> ##[1:1000] data_valid) for "must complete within 1000 cycles," plus a cover property for the eventually case.

Pitfall 4 — Range repetition without considering edge cases

// Edge case 1: `[*0]` matches a zero-cycle pattern (vacuous match)
sequence s_maybe_held;
    valid [*0:5];     // matches if valid is held for 0, 1, 2, 3, 4, or 5 cycles
endsequence
 
// Edge case 2: `[*0:0]` is the empty match — almost always a bug
sequence s_empty;
    valid [*0:0];     // never useful in production
endsequence
 
// Edge case 3: m > n at compile time is illegal
sequence s_illegal;
    valid [*5:2];     // compile error
endsequence

Fix: explicit ranges like [*1:N] (not [*0:N]) when zero-length matches don't make sense for the spec rule. Edge case [*0] is occasionally useful but production discipline usually avoids it for clarity.

Debug Lab — "The Burst Length Assertion Fires on Spec-Legal Bursts"

A subtle failure mode that surfaces when an engineer reaches for [=n] thinking it means "exactly N occurrences" without realising the goto-vs-non-consecutive distinction.

// Spec: "during a burst, exactly 4 data beats are transferred,
//        each marked by data_valid; burst_end follows the 4th beat"
//
// Engineer's translation:
property p_burst_4_beats;
    @(posedge clk) disable iff (rst)
        $rose(burst_start) |->
            data_valid [=4] ##1 burst_end;
endproperty

*E,ASRTST: [9ns] p_burst_4_beats failed
   data_valid [=4] matched at cycle 8, but burst_end not at cycle 9
   (the match extends further)

// Spec: "during a burst, exactly 4 data beats are transferred,
//        each marked by data_valid; burst_end follows the 4th beat"
//
// Translation: anchor on the 4th occurrence of data_valid
property p_burst_4_beats;
    @(posedge clk) disable iff (rst)
        $rose(burst_start) |->
            data_valid [->4] ##1 burst_end;
endproperty

Industry Context — Where Repetition Operators Earn Their Place

• AMBA AXI burst-length contracts. "Burst must transfer 1–256 beats" maps to [*1:256] with data_valid as the boolean. Every AXI VIP encodes this rule as a consecutive repetition with the burst-length range from the protocol's len field.
• PCIe credit-return protocols. "Posted Header credit returns must be cumulative" — counted by [=n] non-consecutive repetition with credit_return as the event boolean. Used in formal flows to prove credit-counter invariants.
• DDR refresh interval verification. "DRAM must be refreshed at least every tREFI" — encoded as [*1:tREFI] for the refresh-trigger boolean. Vendor controllers' assertion files use range repetition with the JEDEC timing constant.
• Error-recovery state machines. "After 3 consecutive timeouts, the link enters retraining" — timeout [*3] chained with ##1 retraining is the canonical encoding. The consecutive operator is correct because the spec specifies consecutive timeouts.
• Cache coherence retry sequences. "After the 5th coherence retry, escalate to bus-wide invalidation" — uses [->5] for the goto-anchor pattern; the chained next step is the escalation event on the cycle after the 5th retry.
• Watchdog timer contracts. "Watchdog timer must reach max value with no reset within the window" — [*WD_PERIOD] consecutive with !reset as the boolean is the natural encoding.

The pattern across these uses: the repetition operator is matched to the spec's exact temporal counting semantics. Consecutive duration → [*n]; total-count-without-consecutivity → [=n]; chained-pattern-anchored-on-Nth → [->n]. The production discipline is to read the spec's wording explicitly for each repetition operator choice.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Repetition-Operator Discipline

1. Match the operator to the spec's exact temporal counting wording. "Consecutive" / "in a row" → [*n]. "N total" / "anywhere" → [=n]. "On the Nth, then X" → [->n].
2. Use [->n] for chained patterns. When a ##1 next_event follows the repetition, the next event must anchor on the Nth occurrence — [->n] provides that anchor. [=n] lets the match extend past the Nth occurrence, usually producing the wrong contract.
3. Range forms are the workhorse — prefer [*1:N] over [*N] when the spec allows a range. Spec rules often have implicit ranges ("1 to N cycles"); the range form encodes them directly.
4. Pair every unbounded-repetition assertion with a hard-deadline backup. [*1:$] and [=1:$] don't enforce a deadline; the unbounded forms can vacuously pass if the simulation ends without the boolean firing again. A separate assert property (... |-> ##[1:K] ...) enforces the bound.
5. Document the repetition-operator choice with a spec-section citation. "Spec §6.2: 'data_valid must hold for 4–16 consecutive cycles during a burst'" — the citation traces the operator choice to the spec rule it encodes.
6. Pair every spec-critical repetition assertion with a cover of the antecedent. The cover hit count confirms the assertion's antecedent fired in the regression — needed to distinguish "passing because contract honored" from "passing because antecedent never fired."
7. When debugging an assertion that fires on a spec-legal scenario, audit the repetition operator first. The [=n]-vs-[->n] distinction is the most common chained-pattern bug; checking the operator choice before debugging the testbench saves hours.

Summary

The three repetition operators — [*n] consecutive, [=n] non-consecutive, [->n] goto — and their range forms [*m:n], [=m:n], [->m:n] are how SVA encodes multi-cycle counting and duration contracts. [*n] is for consecutive-duration spec rules; [=n] for total-count rules where occurrences can be scattered; [->n] for chained patterns where the Nth occurrence anchors the next step. The single most common production bug is using [=n] for a chained pattern when [->n] was meant — the matching window extends past the Nth occurrence, allowing the next step to fire at the wrong cycle. Match each operator to the spec's exact wording, document the choice with a spec citation, and pair every repetition assertion with a cover of the antecedent. Module 12.10 builds on this with the full assert / assume / cover / restrict construct semantics — the verbs that complete the SVA grammar.