Verification

SystemVerilog Assertions — a practical guide

SystemVerilog Assertions (SVA) let you state, in the design itself, what must always be true and what must never happen — then check it automatically in simulation or prove it in formal. A good assertion is a specification that fails loudly the instant reality drifts from intent. This guide walks through the two flavors of assertion, the property and sequence layer that makes temporal checks possible, the operators you will reach for daily (|->, |=>, ##N, $rose, $past, disable iff), and the one failure mode that quietly makes assertions lie: a vacuous pass.

Immediate vs concurrent assertions

SVA comes in two forms, and confusing them is the most common beginner mistake. An immediate assertion is a procedural statement — it lives inside an always or initial block and evaluates a plain Boolean expression at the moment control reaches it, exactly like an if. It is perfect for invariants you can check from a single instant's values: a one-hot select, a FIFO that is never simultaneously full and empty, a pointer that stays in range.

// Immediate assertion: a procedural check, evaluated when this line runs.
always_comb begin
    if (sel == 2'b11)
        data = c;
    // The FIFO must never be full and empty at once.
    assert (!(full && empty))
        else $error("fifo: full and empty asserted together");
end

A concurrent assertion is a different animal. It is clocked — sampled on a specified edge — and it can describe behavior that unfolds over multiple cycles. This is what lets you write “every request is granted within three cycles” or “valid never drops before ready.” Concurrent assertions read values using the sampled-value semantics (the value just before the clock edge), which avoids the race conditions that plague ad-hoc checker code. When people say “SVA” they almost always mean concurrent assertions, because the temporal expressive power is the whole point.

The property and sequence layer

Concurrent assertions are built in layers. A sequence describes a pattern of Boolean values across consecutive clock ticks. A property wraps sequences with implication, negation, and clocking to form a complete statement of intent. You then bind a property to a verification directive — assert, assume, or cover — to say what to do with it.

// Concurrent assertion: sampled on posedge clk, checked over time.
// "A request must be granted within 1 to 3 cycles, unless reset."
property req_granted;
    @(posedge clk) disable iff (!rst_n)
        req |-> ##[1:3] gnt;
endproperty

assert property (req_granted);

// cover the antecedent so a vacuous pass cannot hide:
cover property (@(posedge clk) req);

The cycle-delay operator ##N advances the sequence by N clock ticks; ##[1:3] is a range, matching anywhere from one to three cycles later. The disable iff clause aborts evaluation when its condition is true — almost always tied to reset, so an assertion does not fire spuriously while the design is being held in reset.

Implication: |-> vs |=>

Implication is the backbone of nearly every useful property. It splits a property into an antecedent (the trigger, on the left) and a consequent (the obligation, on the right). The property only imposes a requirement when the antecedent matches; otherwise it is trivially satisfied. Hold that thought — it is the root of vacuity.

• Overlapping, |-> — the consequent is evaluated on the same clock tick the antecedent completes. Use it when the response is simultaneous with the trigger: write |-> !read.
• Non-overlapping, |=> — the consequent is evaluated on the next clock tick. It is exactly equivalent to |-> ##1. Use it for next-cycle responses: req |=> busy.

Sampled-value functions: $rose, $fell, $stable, $past

Real protocols care about edges and history, and SVA gives you helper functions that read the sampled value of an expression relative to the clock. $rose(sig) is true on the tick where sig went 0→1; $fell(sig) is the opposite; $stable(sig) is true when the value did not change since the previous tick; and $past(sig, N) returns the value sig held N cycles ago (N defaults to 1). These let you express “data must not change while valid is high” or “the counter increments by one each accepted beat” directly.

// Sampled-value functions describe edges and history.
// "If valid rises, data must be stable until the cycle ready is high."
property valid_data_stable;
    @(posedge clk) disable iff (!rst_n)
        $rose(valid) |=> $stable(data) until ready;
endproperty
assert property (valid_data_stable);

// $past looks back: the address increments by one each accepted beat.
assert property (@(posedge clk) disable iff (!rst_n)
    (beat_ack) |-> (addr == $past(addr) + 1));

assert vs assume vs cover

The same property means very different things depending on the directive you bind it to:

• assert property — an obligation on the design. If the property is violated, the tool reports a failure with the offending cycle. This is your correctness check.
• assume property — a constraint on the environment. In formal verification, an assume tells the solver which inputs are legal so it does not waste effort (or raise false alarms) on stimulus that can never occur. Misused assumes are dangerous: an over-strong assume can make a buggy design look proven.
• cover property — not a check at all. It records whether a sequence actually happened during the run. Cover is how you measure reachability, and it is the standard antidote to vacuity — cover the antecedent and you will know whether your assertion ever did real work. Cover ties directly into functional coverage closure.

The honesty rule: a vacuous pass proves nothing

Here is the failure mode that quietly turns a green assertion report into a false sense of safety. An implication property antecedent |-> consequent only checks the consequent on cycles where the antecedent is true. If the antecedent is never true during the entire run — because the stimulus never drove that scenario, a typo guarded it away, or a signal name was wrong — then the implication is satisfied vacuously. The assertion passes. It proves nothing, because the behavior it was written to verify never occurred.

A vacuous pass is the assertion-world equivalent of a testbench that runs zero vectors and reports “all tests passed.” The same anti-vacuity discipline shows up in logical equivalence checking, where a proof over zero matched points is also vacuous. The standard defense is to pair every meaningful assertion with a cover property on its antecedent: if the cover never hits, your assertion never fired and the pass is hollow.

This is exactly the distinction ChipVerify AI is built to preserve. We treat a triggered, observed pass as evidence and a vacuous pass as a gap to surface — a property whose antecedent never held is reported as such, never quietly counted as proof. Honest evidence means telling you what was not exercised, not rounding an untriggered property up to “passed.”

SVA on open tools: what is and is not supported

A practical note for open-source flows. Simulators like Verilator and Icarus support immediate assertions and a useful subset of concurrent assertions, while the open Yosys/SymbiYosys formal frontend rejects temporal SVA operators (|->, |=>, ##N, $past, $stable) at module scope. Rather than overclaim full SVA support, ChipVerify AI expresses next-cycle properties on open tools as clocked immediate assertions — the temporal intent is hand-registered into a clocked always block with explicit past-value flops and a reset gate, which the open formal engines accept. You get real, formally-grounded evidence for the properties that matter, produced on open tools — pre-signoff evidence, not a foundry signoff, and not a replacement for a commercial SVA-capable EDA flow.

Assertions are one layer of a complete plan. They pair naturally with a structured verification plan and with broader RTL verification coverage — assertions catch protocol violations, coverage tells you whether you exercised the design enough to trust the green.

FAQ