SVA Sequences

Module 12 · Page 12.5

What a Sequence Is

Module 12.4 introduced concurrent assertions and their property expressions. The property expression is what the assertion checks; this page introduces sequences — the named, reusable, composable building blocks that property expressions are built from. A sequence is a temporal pattern: "this happened, then this happened N cycles later, then this." Once a sequence is named, it can be reused across many properties, parameterised, composed with other sequences, and shipped as part of a verification IP library.

The conceptual analogy: a sequence is to SVA what a function is to a procedural language. You can write everything inline; you should name and reuse the patterns you write more than once. Production verification environments have sequence libraries — seq_apb_read, seq_axi_burst, seq_pcie_tlp — that turn each protocol's temporal vocabulary into named building blocks the assertions compose.

Declaring a Sequence

A sequence is declared with sequence ... endsequence. The sequence has a name, an optional argument list, a clocking specification (optional — inherits from the using property), and a temporal expression body.

// ── Simple sequence — fixed temporal pattern ────────────────────
sequence s_req_then_ack;
    req ##1 ack;     // req high in cycle N, ack high in cycle N+1
endsequence
 
// ── Parameterised sequence — accepts arguments ─────────────────
sequence s_req_then_ack_in(int unsigned delay);
    req ##delay ack;
endsequence
 
// ── Sequence with its own clocking ─────────────────────────────
sequence s_handshake;
    @(posedge clk) req ##1 ack ##1 done;
endsequence
 
// ── Using sequences in properties and assertions ──────────────
property p_handshake_completes;
    @(posedge clk) disable iff (rst)
        s_req_then_ack;             // referenced by name
endproperty
 
a_handshake:
assert property (p_handshake_completes)
    else $error("[%0t] req-ack handshake violation", $time);

The reading rule: a sequence is a named pattern; a property gates it with clocking, disable conditions, and implication; the assertion construct enforces or measures the property. Each layer adds semantics the previous didn't have.

Delay Operators — ##n and ##[m:n]

The ## operator is the temporal glue inside a sequence — it specifies how many clock cycles separate consecutive boolean conditions.

// ── Fixed delays ────────────────────────────────────────────────
sequence s_exact_2_cycles;
    req ##2 ack;     // ack exactly 2 cycles after req
endsequence
 
sequence s_same_cycle;
    req ##0 grant;   // both high in the same cycle
                      // (equivalent to req && grant in that cycle)
endsequence
 
// ── Range delays — protocol latency windows ─────────────────────
sequence s_apb_pready_window;
    $rose(penable) ##[1:16] pready;   // pready within 1–16 cycles
endsequence
 
sequence s_eventual_completion;
    req ##[1:$] done;                  // done eventually, no upper bound
endsequence
 
// ── Chained delays — multi-step sequences ──────────────────────
sequence s_three_step_pipeline;
    start ##1 stage1 ##1 stage2 ##1 done;
    // start at cycle N, stage1 at N+1, stage2 at N+2, done at N+3
endsequence

The range form ##[m:n] is the workhorse for protocol-latency assertions — "the response arrives within K cycles" is the most common shape, and the range form encodes it directly without enumerating every possible delay. The unbounded form ##[1:$] (sometimes written ##[1:$]) is for eventual-completion properties — useful when the spec says "eventually" without a hard deadline, though production discipline usually pairs it with a separate hard-deadline assertion for the real spec requirement.

Composition Operators — and, or, intersect

Sequences compose. SVA provides three operators to combine them.

and — both sequences match, possibly different lengths

sequence s_a_within_5;
    a ##[1:5] complete_a;
endsequence
 
sequence s_b_within_8;
    b ##[1:8] complete_b;
endsequence
 
sequence s_both_complete;
    s_a_within_5 and s_b_within_8;
    // Both sequences must match — starting from the same cycle.
    // They can end at different cycles; the combined sequence
    // ends at the LATER of the two end cycles.
endsequence

Use and for "both these things must happen, in any timing relationship to each other." Common in multi-channel protocol checks where two independent operations must both complete.

or — either sequence matches

sequence s_success_or_error;
    (req ##[1:10] ack) or (req ##[1:5] err);
    // Either ack arrives within 10 cycles after req,
    // OR err arrives within 5 cycles after req.
endsequence

Use or for "any one of these acceptable responses is fine." Common in protocols with multiple legal response types (OKAY vs EXOKAY for AXI; READY vs ERROR for many bus protocols).

intersect — both sequences match AND end at the same cycle

sequence s_a_in_5;
    a ##[1:5] complete_a;
endsequence
 
sequence s_b_in_8;
    b ##[1:8] complete_b;
endsequence
 
sequence s_simultaneous_completion;
    s_a_in_5 intersect s_b_in_8;
    // Both sequences must match AND must end on the same cycle.
    // Much stronger constraint than `and`.
endsequence

Use intersect for "both these things must happen, and they must finish at the same time." Less common than and; useful for verifying synchronization points where two independent operations must complete simultaneously.

first_match — keep only the earliest match of a sequence

sequence s_first_complete;
    first_match(req ##[1:$] complete);
    // The sequence matches on the EARLIEST cycle where complete fires
    // after req. Later matches in the same range are suppressed.
endsequence

Use first_match for "we care about the first occurrence, not subsequent ones." Common in implication antecedents where matching multiple times for the same trigger would cause duplicate checks.

throughout — a condition must hold for the duration of a sequence

sequence s_busy_throughout_burst;
    busy throughout (start ##[1:$] done);
    // For the entire duration from `start` to the first `done`,
    // `busy` must be continuously high.
endsequence
 
// More common shape — express the contract directly:
property p_busy_during_burst;
    @(posedge clk) disable iff (rst)
        start |-> (busy throughout (1'b1 ##[1:$] done));
endproperty

Use throughout for "this signal must hold continuously for the duration of that pattern." Common for hold-during-transfer rules: "AWVALID must be held throughout the address phase," "DATA must be stable throughout the wait-state window."

Boolean Conditions Inside Sequences

The atomic unit inside a sequence is a boolean expression — a same-cycle condition over the design's signals. Anything legal in a SystemVerilog if is legal inside a sequence's boolean position.

sequence s_complex_boolean;
    // Any boolean expression is legal here
    (req && valid && !err) ##1 (ack && !pending);
endsequence
 
sequence s_using_system_functions;
    // SVA system functions provide useful temporal primitives
    $rose(start) ##1 $stable(data) ##1 $fell(busy);
    // $rose(x): true when x transitions 0->1 at this clock edge
    // $fell(x): true when x transitions 1->0 at this clock edge
    // $stable(x): true when x has the same value as last clock edge
    // $past(x, N): the value of x N cycles ago
endsequence
 
sequence s_using_past;
    enable && ($past(enable) == 1'b0);   // enable just turned on
endsequence

The four SVA-specific functions $rose, $fell, $stable, and $past are the workhorses for edge-detection and history-aware conditions inside sequences. They make protocol-spec encoding direct: "AWREADY rose" is $rose(awready), not the more verbose awready && !$past(awready).

A Complete Working Example — APB Sequence Library

The pattern below is the canonical production shape: a small reusable sequence library for an AMBA APB protocol, with the protocol's spec rules encoded as named sequences that assertions and cover properties compose.

package apb_sequences;
    // ── Atomic sequences — the building blocks ───────────────────
 
    sequence s_apb_setup_phase(input bit psel, penable);
        psel && !penable;   // PSEL high, PENABLE low — APB SETUP phase
    endsequence
 
    sequence s_apb_access_phase(input bit psel, penable);
        psel && penable;    // PSEL high, PENABLE high — APB ACCESS phase
    endsequence
 
    sequence s_apb_idle(input bit psel);
        !psel;              // PSEL low — APB IDLE
    endsequence
 
    // ── Multi-step sequences — full transfers ───────────────────
 
    sequence s_apb_write_transfer(input bit psel, penable, pwrite, pready);
        // SETUP → ACCESS → wait for PREADY (up to 16 cycles) → IDLE
        (s_apb_setup_phase(psel, penable) && pwrite) ##1
        (s_apb_access_phase(psel, penable) && pwrite) ##[0:15]
        (pready) ##1
        s_apb_idle(psel);
    endsequence
 
    sequence s_apb_read_transfer(input bit psel, penable, pwrite, pready);
        (s_apb_setup_phase(psel, penable) && !pwrite) ##1
        (s_apb_access_phase(psel, penable) && !pwrite) ##[0:15]
        (pready) ##1
        s_apb_idle(psel);
    endsequence
endpackage
 
// ── Assertions and covers using the library ──────────────────────
module apb_slave_assertions (
    input  bit clk, rst_n,
    input  bit psel, penable, pwrite, pready
);
    import apb_sequences::*;
 
    // ── Assertion: every SETUP must be followed by ACCESS ───────
    a_setup_to_access:
    assert property (@(posedge clk) disable iff (!rst_n)
        s_apb_setup_phase(psel, penable) |=>
        s_apb_access_phase(psel, penable))
        else $error("[%0t] SETUP not followed by ACCESS", $time);
 
    // ── Cover: write transfer was exercised ──────────────────────
    c_write_transfer:
    cover property (@(posedge clk) disable iff (!rst_n)
        s_apb_write_transfer(psel, penable, pwrite, pready));
 
    // ── Cover: read transfer was exercised ──────────────────────
    c_read_transfer:
    cover property (@(posedge clk) disable iff (!rst_n)
        s_apb_read_transfer(psel, penable, pwrite, pready));
 
    // ── Assertion: PREADY arrives within 16 cycles of ACCESS ────
    a_pready_within_16:
    assert property (@(posedge clk) disable iff (!rst_n)
        s_apb_access_phase(psel, penable) |-> ##[0:15] pready)
        else $error("[%0t] PREADY timeout: > 16 cycles in ACCESS phase",
                     $time);
endmodule

What this code does. Declares a package of reusable APB sequences — three atomic state sequences and two multi-step transfer sequences. The assertions and cover properties compose these named sequences instead of re-encoding the protocol rules inline. Result: the protocol vocabulary is centralised in one place; multiple DUTs and verification environments share the same s_apb_write_transfer definition. If the spec changes ("ACCESS phase extended to 32 cycles"), one edit to one sequence updates every assertion that uses it.

How to simulate it. Compile the package + assertion module + DUT. Run an APB-protocol regression with reads, writes, back-pressure, and error injection. Assertions fire on real protocol violations; cover properties confirm that read and write transfers were exercised.

Expected output (fragment).

# *E,ASRTST: [142] PREADY timeout: > 16 cycles in ACCESS phase
#   a_pready_within_16 failed at 142ns
#
# Coverage summary:
#   c_write_transfer: 87 hits  (write transfer pattern matched)
#   c_read_transfer:  43 hits  (read transfer pattern matched)
#
# Total assertion failures: 1

What to read out of this. One spec violation, two cover patterns exercised. The library pattern's payoff is visible: the assertion's failure message references the protocol-level sequence name (a_pready_within_16), not the raw signal-level conditions; the cover properties confirm the regression exercised both transfer types. A new engineer reading this code without prior APB knowledge can recover the protocol's rules from the sequence names alone — s_apb_setup_phase, s_apb_access_phase, s_apb_write_transfer self-document.

Common Pitfalls

Pitfall 1 — Using and when intersect is meant (or vice versa)

// Intent: a-pattern and b-pattern both complete, doesn't matter when
sequence s_intent;
    (a ##[1:5] complete_a) intersect (b ##[1:8] complete_b);
    // BUG: intersect requires SAME end cycle — both must finish
    // exactly together. Almost never what you want.
endsequence
 
// Right form:
sequence s_correct;
    (a ##[1:5] complete_a) and (b ##[1:8] complete_b);
    // and allows different end cycles — both just have to match.
endsequence

Fix: and allows different end cycles ("both happened"); intersect requires same end cycle ("both happened AND finished simultaneously"). The misuse silently makes the sequence almost-never-match, hiding real coverage gaps as "the cover never fires because the scenario is impossible."

Pitfall 2 — Forgetting first_match causes duplicate antecedent firings

property p_eventually_done;
    @(posedge clk) (req ##[1:$] done) |=> ack;
    // The antecedent (req ##[1:$] done) can match many times for one req
    // — once at the first done, again at the second done, etc.
    // The implication fires for every match.
endproperty
 
// Better — use first_match to match only the first done after req:
property p_eventually_done_first;
    @(posedge clk) first_match(req ##[1:$] done) |=> ack;
endproperty

Fix: when the antecedent uses ##[m:$] or ##[m:n] with broad ranges, wrap it in first_match(...) to suppress multiple matches for the same trigger.

Pitfall 3 — Unbounded sequences without a hard-deadline backup assertion

// Intent: req must be followed by ack
property p_eventually_ack;
    @(posedge clk) req |-> ##[1:$] ack;
    // PASSES if ack arrives in 1, 1000, 100000 cycles — or never within the
    // simulation. SVA's `##[1:$]` matches only WITHIN the simulation; if the
    // simulation ends before ack, the property is vacuous, not failing.
endproperty

Fix: unbounded ##[m:$] doesn't enforce a deadline — it just allows any positive delay. Production discipline pairs the unbounded form with a separate hard-deadline assertion: assert property (req |-> ##[1:1000] ack) for "must complete within 1000 cycles," plus a cover property for the eventually case.

Pitfall 4 — Naming sequences for signals instead of for spec rules

sequence s_signal_req_then_signal_ack;   // describes signals
    req ##1 ack;
endsequence
 
// vs.
 
sequence s_apb_handshake_complete;        // describes the protocol rule
    req ##1 ack;
endsequence

Fix: name sequences for the protocol or spec rule they encode, not for the signals they reference. The signal-named version goes stale if the design's signal names change; the protocol-named version stays meaningful as the contract document.

Debug Lab — "The Cover Property Never Fires"

A subtle failure mode that catches engineers writing their first sequence library: the cover property reports zero hits, the team assumes the test never exercises the scenario, hours of stimulus debugging follow — but the real bug is in the sequence definition.

sequence s_write_arrives;
    awvalid ##[1:5] awready;
endsequence
 
sequence s_data_arrives;
    wvalid ##[1:8] wready;
endsequence
 
// BUG: intersect requires both sequences to END at the same cycle
// Address handshake completes in 1-5 cycles
// Data handshake completes in 1-8 cycles
// They almost never align exactly — intersect is the wrong operator
c_write_burst:
cover property (@(posedge clk) disable iff (!rst_n)
    s_write_arrives intersect s_data_arrives);

c_write_burst:
cover property (@(posedge clk) disable iff (!rst_n)
    s_write_arrives and s_data_arrives);
    // `and` requires both sequences to match starting from the same cycle,
    // but they may end at different cycles.

Industry Context — Where Sequence Libraries Live

• AMBA protocol VIPs. Every shipping AXI / AHB / APB VIP includes a sequence library — s_axi_aw_handshake, s_axi_b_response, s_apb_full_transfer. The library is the protocol vocabulary that the VIP's assertions and covers compose. Integrators reuse the sequences in their own custom assertions, not just the VIP's.
• PCIe LTSSM verification. Each LTSSM state transition is a named sequence; the property file composes them into the full state-graph contract. Formal flows use the sequences as inputs to compositional model-checking — proving "state X always reaches state Y within K cycles" by decomposing the full proof into per-sequence sub-proofs.
• DDR / LPDDR command sequencing. JEDEC timing parameters (tRCD, tRP, tRC, tFAW) become named sequences in the controller's assertion library. The spec's timing table maps one-for-one to the sequence library, so any spec revision becomes a sequence-edit instead of a re-derivation of every assertion.
• UVM monitor's protocol-decoder layer. UVM monitors invariably include a sequence library that decodes signal-level events into transaction-level events; the same sequences power both the assertion checking and the transaction-class field reconstruction. The dual-use means the protocol contract is centralised in one place.
• Cross-design protocol reuse. When a company has multiple chips using the same internal bus protocol, the bus's sequence library is published as an internal package. All chips' assertion files compose the shared sequences; any protocol clarification is one library edit propagating to every consumer.

The pattern across these uses: production verification environments treat sequence libraries as a first-class deliverable — versioned, documented, reviewed independently of any single chip. The library is what makes protocol expertise portable across projects.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for Sequence Discipline

1. Name sequences for the spec rule they encode, not for the signals they reference. s_apb_handshake_complete survives a signal rename; s_signal_req_then_signal_ack doesn't.
2. Build a sequence library in a package; import it into every assertion module that uses the protocol. Centralised vocabulary, single point of edit, consistent enforcement across the verification environment.
3. Default to and for "both happened" composition; use intersect only with a documented spec citation. Most intersect uses in real codebases are bugs.
4. Wrap broad-range antecedents in first_match(...) when the antecedent should fire once per trigger. Avoids duplicate implications for the same req.
5. Pair unbounded ##[m:$] sequences with a hard-deadline assertion. "Eventually" isn't an enforceable deadline; the unbounded form is for cover or for spec-flexible properties, not for the hard-timeout case.
6. Use $rose, $fell, $stable, $past directly instead of equivalent boolean expressions. The SVA system functions are more readable, match spec language more closely, and produce better assertion-failure messages.
7. When a cover reports 0 hits, debug the sequence structure before the stimulus. Print the antecedent's signal values in a parallel $display to distinguish "structure broken" from "scenario never reached" in minutes.

Summary

Sequences are SVA's reusable temporal-pattern building blocks. The sequence ... endsequence declaration names a pattern; properties and assertions reference the named sequence instead of re-encoding the pattern inline. The ##n and ##[m:n] delay operators glue boolean conditions across cycles; and, or, intersect, first_match, and throughout compose sequences into larger patterns. The four SVA system functions ($rose, $fell, $stable, $past) encode edge-detection and history-aware conditions inside sequences. Production verification environments treat sequence libraries as first-class deliverables — versioned, documented, reused across chips. The most common pitfall is using intersect where and was meant; the most common debug session is "cover reports 0 hits" where the bug is in the sequence structure, not the stimulus. Module 12.6 builds on this with properties — the named-contract layer that composes sequences with implication and disable conditions.