Introduction to SystemVerilog Assertions (SVA)

Module 12 · Page 12.1

The Temporal Contract Layer

Module 11 built functional coverage — the metric that answers "did we exercise every spec scenario?" Module 12 builds the complementary layer: SystemVerilog Assertions, or SVA. Where coverage measures whether scenarios were tested, SVA enforces whether the design's behaviour matches the spec while those scenarios were running. Coverage is the scoreboard; SVA is the referee.

An assertion is an executable specification — a statement in the design (or in a separate bind file) that declares "this property must always hold." The simulator (or a formal tool) evaluates the assertion continuously: every clock cycle, every transaction, every time the property's antecedent fires. If the property is ever false, the assertion fails — and the failure carries the exact time and signal values that made it fail. No waveform hunting. No "the bug propagated for 50 cycles before we saw it." The violation surfaces at the source.

Why SVA Earns Its Place — the Bug-Hunt Problem

The single most expensive failure mode in non-trivial verification is late bug discovery. An illegal RTL state at cycle 3 corrupts the pipeline; the corruption propagates silently through five stages; at cycle 8, an output is wrong; the scoreboard flags the mismatch. The engineer now has cycles 3 through 8 of waveform to hunt through, with no guidance about which cycle was the root cause.

cycle:    0     1     2     3            4     5     6     7     8
clk:    ┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└┘
state:  IDLE  REQ   REQ   ILLEGAL!     PROC  PROC  DONE  IDLE  → output 0xFF (WRONG)
                          ↑                                       ↑
                          root cause                              symptom (scoreboard fail)
                          (silent — never reported)

The same scenario with one SVA assertion on the FSM transition contract:

cycle:    0     1     2     3
clk:    ┘└┘└┘└┘└┘└┘└┘└┘
state:  IDLE  REQ   REQ   ILLEGAL!
                          ↑
                          $error: "Illegal state transition at time 30ns;
                                    state=2'b11 is not in spec-defined set"
                          (simulation stops if $fatal; logged if $error)

The assertion captures the contract once, in one line of code, and watches every clock cycle for the rest of simulation. The cost is the line of code; the payoff is the difference between "five cycles of corrupt propagation to trace" and "the violation is reported with the offending value at the offending time."

Where SVA Lives

Assertions appear at every layer of a verification environment, but the natural places are six:

Each of these has a procedural-code equivalent — a manually-maintained if (...) $error(...) somewhere in the testbench. The SVA form is shorter, runs continuously, and survives refactors that would break the procedural equivalent.

Immediate vs Concurrent — The Two Assertion Forms

SVA has two structurally different assertion forms. They suit different verification questions.

Immediate assertions

An immediate assertion is evaluated right now — at the point of execution, like an if statement. Used inside always blocks, initial blocks, tasks, and functions. Purely combinational; no clock involvement. The right tool for "check that this condition holds at this instant" — data validity, range checks, function-precondition checks.

always @(posedge clk) begin
    if (push && !pop) begin
        // ── Immediate assertion: checks count < DEPTH right now ────
        assert (count < DEPTH)
            else $error("FIFO overflow attempt at time %0t (count=%0d)",
                        $time, count);
        count <= count + 1;
    end
end

The semantics: the assertion fires the moment execution reaches the assert statement. If count < DEPTH is true, the assertion silently passes; if false, the else action block runs ($error in this example). Module 12.2 covers immediate assertions in detail.

Concurrent assertions

A concurrent assertion runs in parallel with the design, evaluating its property on every clock edge (or other declared event). Clock-driven by construction. The right tool for temporal contracts — "if A happens, then B must follow within N cycles," "no two transitions of these signals in the same cycle," "this state lasts exactly M cycles."

// Named property — the spec-row form, reusable
property p_req_ack;
    @(posedge clk) disable iff (rst)
        req |=> ack;             // if req high, ack must be high next cycle
endproperty
 
// Assertion that enforces the property
a_req_ack:
assert property (p_req_ack)
    else $error("REQ at %0t not acknowledged the following cycle", $time);

The semantics: every posedge clk, the simulator evaluates the property. If rst is high, the evaluation is disabled (the disable iff clause). Otherwise, if req is high in this cycle, ack must be high in the next cycle (|=> — non-overlapping implication). The assertion fires as soon as any window violates the contract. Modules 12.4 through 12.9 build out the concurrent-assertion vocabulary.

The Four SVA Constructs — assert, assume, cover, restrict

All four constructs use the same property/sequence language. They differ in what they do when evaluated.

The most important distinction at the intro level is assert vs cover — they have opposite logic:

• assert property (req |=> ack) — fails when the property is false (i.e., when req happened and ack didn't follow). Used to catch bugs in the design's response.
• cover property (req |=> ack) — records a hit when the property is true (i.e., when the handshake did happen). Used to measure whether the scenario was ever exercised by the regression.

The same property req |=> ack can appear in both forms — once as assert (the bug-catcher) and once as cover (the coverage measurer). Production environments often use both, providing complete spec coverage of "the handshake works when it happens" and "the handshake happens often enough to verify it."

// ── assert: catches bugs ─────────────────────────────────────────
a_req_ack:
assert property (@(posedge clk) disable iff (rst)
    req |=> ack)
    else $error("REQ at %0t not acknowledged next cycle", $time);
 
// ── assume: constrains formal tool inputs (sim treats like assert) ─
m_no_simultaneous_rw:
assume property (@(posedge clk)
    !(read && write));    // formal: env will never drive both high
 
// ── cover: measures whether the scenario was exercised ────────────
c_handshake_seen:
cover property (@(posedge clk)
    req ##1 ack);          // count how many times this happened
 
// ── Named assertions/covers make reports readable ────────────────
c_full_xn:
cover property (@(posedge clk)
    req ##1 ack ##1 done); // full three-cycle scenario

The naming convention a_* / m_* (assume) / c_* is widespread in production codebases and makes assertion logs grep-friendly — a verification engineer scanning a regression failure list can immediately tell which entries are bug catches vs which are coverage hits.

A Working Example — One Property, Three Constructs

The pattern below shows how the same temporal property req |=> ack serves three roles in a complete verification environment.

module dut_with_sva (
    input  bit clk,
    input  bit rst,
    input  bit req,
    output bit ack
);
    // DUT logic — simplified
    always_ff @(posedge clk or posedge rst) begin
        if (rst)        ack <= 1'b0;
        else if (req)   ack <= 1'b1;     // ack one cycle after req
        else            ack <= 1'b0;
    end
 
    // ── The spec property — req must be followed by ack next cycle ──
    property p_req_ack;
        @(posedge clk) disable iff (rst)
            req |=> ack;
    endproperty
 
    // ── Role 1 — assert: fires if the DUT violates the contract ────
    a_req_ack:
    assert property (p_req_ack)
        else $error("[%0t] REQ not acknowledged next cycle", $time);
 
    // ── Role 2 — cover: confirms the scenario was exercised ────────
    c_req_ack_hit:
    cover property (p_req_ack);
 
    // ── Role 3 — assume: in formal, constrains env to drive req
    //            in spec-legal ways (here: not during the first
    //            two cycles after reset, per spec §4.1)
    // synthesis-pragma: formal-only
    m_req_quiet_after_reset:
    assume property (@(posedge clk) disable iff (!rst_history_seen)
        $past(rst, 2) |-> !req);
endmodule

What this code does. Defines the spec property once (p_req_ack). The assert form enforces it — any cycle where req is high without ack following next cycle fires $error. The cover form measures it — every successful (req, ack) handshake increments a coverage counter, so the regression report can prove the scenario was exercised. The assume form constrains formal inputs — in a formal flow, the engine will not search input sequences where req rises within two cycles of reset deassertion.

How to simulate it. Compile under any IEEE 1800-compatible simulator with SVA enabled (vcs -sverilog -assert enable_diag, vsim -assertdebug, xrun -access +r -coverage all). Drive realistic stimulus and observe both the assertion log and the cover-property hit counts.

Expected output (assertion log + cover report).

# *E,ASRTST: [25] REQ not acknowledged next cycle
#   Property p_req_ack failed at 25ns
#   Antecedent fired at 25ns; consequent expected high at 35ns; was low
 
# Coverage summary:
#   c_req_ack_hit:    442 hits   (handshake scenario exercised 442 times)
#   a_req_ack:          1 fail   (one violation at 25ns)

What to read out of this. The cover property tells you the scenario was exercised 442 times. The assert tells you that of those 442 attempts, 441 succeeded and one failed — at 25ns, after req rose, ack did not follow next cycle. The verification engineer's next step is to read the waveform at 25ns and trace why the DUT's ack logic didn't respond. The pairing of assert and cover for the same property gives both bug evidence and exercise evidence — which is exactly what a verification audit needs.

Quick Preview — Temporal Operators

Concurrent assertions get most of their power from a small set of temporal operators. The full vocabulary lives in Modules 12.5 (sequences) through 12.9 (repetition); the preview is for orientation.

// ── Fixed delay — ack exactly 2 cycles after req ─────────────────
assert property (@(posedge clk) req |-> ##2 ack);
 
// ── Range delay — grant arrives within 1–10 cycles ──────────────
assert property (@(posedge clk) req |-> ##[1:10] gnt);
 
// ── Consecutive repetition — valid high for 4 cycles ────────────
assert property (@(posedge clk) start |-> valid[*4]);
 
// ── Range repetition — burst lasts 2–8 cycles, then done ────────
assert property (@(posedge clk)
    burst_start |-> busy[*2:8] ##1 burst_done);

These four examples cover most basic protocol-temporal contracts. AXI's "address-before-data" rule, AHB's "wait-states ≤ 16" rule, APB's "two-cycle SETUP+ACCESS" rule — every one of them is one or two lines of SVA using just these operators.

Common Pitfalls — The Anti-Patterns to Avoid

Pitfall 1 — Forgetting disable iff (rst)

// ── BUG: no disable iff (rst) — assertion fires during reset ─────
assert property (@(posedge clk) req |=> ack);
 
// During reset, the DUT's req/ack are X. The implication's antecedent
// (req) is X. Behaviour depends on the simulator — some treat X as false
// (assertion passes vacuously), some treat X as a violation. Either way,
// you get noise during reset that hides real failures after reset.

Fix: every concurrent assertion that touches signals which are X or in-reset values must include disable iff (rst) (or the equivalent reset-disable clause). Module 12.7 covers this in detail.

Pitfall 2 — Confusing |-> and |=>

// Intent: ack one cycle after req
// Wrong:
assert property (@(posedge clk) req |-> ack);
// Reads: "when req is high, ack must be high in the SAME cycle"
// → fires if the DUT's ack is one-cycle-delayed, even though that's spec-correct
 
// Right:
assert property (@(posedge clk) req |=> ack);
// Reads: "when req is high, ack must be high the NEXT cycle"

Fix: |-> is overlapping (same cycle); |=> is non-overlapping (next cycle). The choice is part of the property's contract — getting it wrong by one cycle is the most common SVA debugging session a new user encounters.

Pitfall 3 — Using immediate assertions for temporal properties

// Intent: ack must follow req next cycle
// Wrong (immediate assertion inside an always block):
always @(posedge clk) begin
    if (req)
        assert (ack);   // fires same cycle, doesn't capture the temporal contract
end
 
// Right (concurrent assertion):
assert property (@(posedge clk) req |=> ack);

Fix: use immediate assertions for same-instant properties (data validity, range checks). Use concurrent assertions for temporal properties (anything involving "next cycle," "within N cycles," "for M consecutive cycles"). Module 12.2 / 12.4 covers when each form is right.

Pitfall 4 — Anonymous assertions

// Wrong (anonymous — the report log can't tell which one failed):
assert property (@(posedge clk) req |=> ack);
assert property (@(posedge clk) wr |=> done);
 
// Right (named — the report shows the violation by name):
a_req_ack:
assert property (@(posedge clk) req |=> ack);
a_wr_done:
assert property (@(posedge clk) wr |=> done);

Fix: every assertion, cover, and assume property carries a name. The simulator log becomes self-describing, regression failure triage becomes faster, and the assertion-source-code-to-spec-row traceability survives refactors.

Debug Lab — "The Bug Took Two Days to Find, the SVA Would Have Caught It in One Line"

A real failure mode from production. A pipeline stage produces a corrupt result; the corruption propagates four stages downstream; the scoreboard flags a mismatch on a downstream output; the team spends two days walking the waveform backward to find the root cause.

module pipeline_stage (
    input  bit          clk, rst,
    input  bit          valid_in,
    input  bit [31:0]   data_in,
    output bit          valid_out,
    output bit [31:0]   data_out
);
    bit [31:0] data_q;
    bit        valid_q;
 
    always_ff @(posedge clk or posedge rst) begin
        if (rst) begin
            data_q  <= 32'h0000_0000;
            valid_q <= 1'b0;
        end else begin
            // ── BUG: data_q updates regardless of valid_in
            //         valid_q gates the output, but a stale data_q can
            //         propagate when valid_in is low — corrupting the
            //         downstream stage on the cycle valid_q happens to be high
            data_q  <= data_in;          // always updates
            valid_q <= valid_in;
        end
    end
 
    assign data_out  = data_q;
    assign valid_out = valid_q;
 
    // No assertions. Bug propagates silently.
endmodule

module pipeline_stage (
    input  bit          clk, rst,
    input  bit          valid_in,
    input  bit [31:0]   data_in,
    output bit          valid_out,
    output bit [31:0]   data_out
);
    bit [31:0] data_q;
    bit        valid_q;
 
    always_ff @(posedge clk or posedge rst) begin
        if (rst) begin
            data_q  <= 32'h0;
            valid_q <= 1'b0;
        end else begin
            if (valid_in) data_q <= data_in;   // ── FIX: gate on valid_in
            valid_q <= valid_in;
        end
    end
 
    assign data_out  = data_q;
    assign valid_out = valid_q;
 
    // ── SVA enforces the data-integrity contract ─────────────────
    a_data_gated_by_valid:
    assert property (@(posedge clk) disable iff (rst)
        valid_q |-> $stable(data_q) || $past(valid_in))
        else $error("[%0t] data_q changed at cycle %0d without valid_in "
                     + "having been high — data-integrity violation",
                     $time, $time/10);
 
    a_data_follows_valid:
    assert property (@(posedge clk) disable iff (rst)
        valid_in |=> data_q == $past(data_in))
        else $error("[%0t] data_q did not follow data_in after valid_in",
                     $time);
endmodule

Industry Context — Where SVA Is Mandatory

• AMBA protocol verification (AXI / AHB / APB). ARM publishes assertion-based VIPs alongside its bus matrices; the assertions encode every spec rule (handshake ordering, byte-strobe legality, response-channel matching) and run continuously in every simulation that uses the VIP. Integrators inherit the assertions automatically.
• PCIe / USB / Ethernet PHY verification. The protocol specs are temporal contracts — "link training step N must be followed by step N+1 within K cycles," "LTSSM state X cannot transition directly to state Y." SVA is the canonical encoding; formal flows (Cadence Jasper, Synopsys VC Formal) use the same SVA source to prove properties exhaustively.
• Cache coherence (MESI/MOESI/MESIF). Coherence contracts are inherently temporal — "a line in M state cannot be invalidated without a writeback," "two caches cannot hold the same line in M simultaneously." SVA captures the rules; coverage measures whether transitions were exercised; the two together produce sign-off evidence.
• Safety-critical certification (DO-254 / ISO 26262 / ARP4754A). Certifying bodies expect SVA-based formal evidence for safety-critical properties (no double-writes, no metastability propagation, no race-condition windows). Pure simulation coverage is insufficient evidence; SVA-plus-formal closes the gap.
• UVM register-model verification. UVM's RAL (Register Abstraction Layer) ships with assertion templates for register access semantics — "RO fields cannot change due to writes," "self-clearing fields return to 0 after one read." The assertions are bound to the register block automatically.
• Bind files for legacy RTL. SVA can be added to existing RTL without modifying the RTL itself — via bind declarations in a separate assertion file. This is the canonical pattern for IP that ships without SVA but is integrated into a flow that requires it: the integrator adds a bind file with the contracts, and the assertions run alongside the RTL as if they were part of it.

The structural fact behind these uses: SVA is the only mechanism that can enforce temporal contracts continuously across a long simulation. Procedural checks in the testbench can catch contract violations at specific moments the testbench checks; SVA catches them at the moment they happen, with the offending values logged. For any non-trivial protocol, that distinction is the difference between debuggable verification and undebuggable verification.

Interview Q&A — Ten Questions You Will Be Asked

Coding Guidelines — Seven Rules for SVA Discipline

1. Every assertion is named. Prefix a_ for assertions, m_ for assumes, c_ for covers. The names make logs grep-friendly, traceability auditable, and regression triage faster.
2. Every concurrent assertion includes disable iff (rst) (or the equivalent reset clause). Without it, the assertion produces noise during reset that hides real failures after reset.
3. Pair assert with cover for spec-critical properties. The assertion catches violations; the cover proves the scenario was exercised. Sign-off audit needs both.
4. Justify every assume with a cited environmental guarantee. assume property (...) in a formal flow constrains the search space — an unjustified assumption hides bugs. The citation is the audit anchor.
5. Use immediate assertions for instant checks; use concurrent for temporal contracts. Immediate inside an always block can verify "this value is valid right now"; concurrent at module scope verifies "next cycle, in N cycles, for M consecutive cycles." Picking the wrong form leaves either timing-window gaps or undetectable false-positives.
6. Assertions live with the RTL they protect. Same file as the module, or in a clearly-named bind file in the same directory. The contract drift surfaces in PR review when RTL and assertions are visually adjacent.
7. Treat assertions as part of the spec, not as decoration. Reviewers should question any RTL PR that doesn't update the relevant assertions when the contract changes. SVA is executable specification; it ages well only when treated that way.

Summary

SystemVerilog Assertions are executable specifications that enforce design contracts continuously. Immediate assertions check same-instant properties; concurrent assertions check temporal properties across clock cycles. The four constructs — assert, assume, cover, restrict — share one property/sequence language but differ in what they do when evaluated: assert catches bugs, cover measures exercise, assume constrains formal-input, restrict scopes formal-proof search. The temporal operators (##n, |->, |=>, [*n], [*m:n], [->n]) express timing relationships that procedural code would take dozens of lines to encode. Pair SVA with functional coverage from Module 11: coverage proves you exercised every scenario, SVA proves the design honored its contracts while every scenario ran. Module 12.2 starts the build-out with immediate assertions; Module 12.4 onwards covers the concurrent vocabulary that does most of the heavy lifting in real verification environments.

Module 12 Roadmap