Assertion Based Verification

Simulation tells you what your design does for the specific inputs you apply. Assertions tell you what your design must always do — and fire automatically the moment that rule is violated, no matter what stimulus triggered it. Embedding assertions directly in the RTL or testbench turns every simulation run into a continuous correctness check, catching bugs at the exact clock cycle they occur rather than waiting for a wrong output to propagate to a visible symptom.

12 min read | Intermediate Level

What You'll Learn

• What assertions are and why they catch bugs that output checking alone misses
• The difference between immediate and concurrent assertions and where each is used
• How assert, assume, and cover properties serve different roles
• How ABV fits into both simulation and formal verification flows

What is Assertion Based Verification?

An assertion is a statement embedded in RTL or a testbench that describes a property the design must satisfy. During simulation, the simulator evaluates each assertion every clock cycle. If the condition is violated, the assertion fires — printing an error message with the exact simulation time, the assertion name, and the signal values at the point of failure.

The key advantage over scoreboard-based output checking is proximity to the source. A scoreboard checks outputs at the interface of the DUT — by the time an incorrect value appears there, it may have passed through several pipeline stages and multiple blocks of logic. An assertion embedded inside the RTL fires at the exact block and cycle where the invariant broke, making root cause analysis significantly faster.

Immediate Assertions

An immediate assertion is evaluated like a procedural statement — it executes at the point in simulation time where it appears in an always or initial block and checks whether its expression is true at that instant. There is no notion of time sequences or clock edges.

always @(posedge clk) begin
    // Immediate assertion: check that grant is never high when request is low.
    // Evaluated at every rising clock edge, just like the surrounding logic.
    assert (!(gnt && !req))
        else $error("Grant asserted without a request at time %0t", $time);
end

Immediate assertions are straightforward and useful for checking instantaneous conditions: mutual exclusion between control signals, valid state encoding in an FSM, or parameter sanity checks at time zero. They cannot describe relationships that unfold over multiple clock cycles.

Concurrent Assertions

A concurrent assertion is evaluated continuously against a clock and can describe properties that span multiple cycles. It runs in parallel with the rest of the simulation — hence "concurrent" — and uses SystemVerilog Assertion (SVA) property syntax to express temporal relationships.

In short, concurrent assertions use three key constructs:

• sequence — a temporal pattern of signal behavior over one or more clock cycles
• property — a named rule built from sequences, often using implication (|-> or |=>)
• assert property — binds a property to a clock and activates it for continuous checking

The most common pattern is an implication property: "whenever condition A is true, condition B must follow." The overlapping implication operator |-> checks condition B in the same cycle as A. The non-overlapping operator |=> checks condition B one cycle after A.

// Property: whenever a request is raised, an acknowledgement must
// arrive within 1 to 4 clock cycles (inclusive).
property p_req_ack_timeout;
    @(posedge clk) disable iff (!rst_n)
    req |-> ##[1:4] ack;
endproperty

assert property (p_req_ack_timeout)
    else $error("ACK not received within 4 cycles of REQ");

Breaking down the key elements:

• @(posedge clk) — the assertion samples signals and evaluates on every rising clock edge
• disable iff (!rst_n) — the assertion is inactive during reset; violations during reset are not reported
• req |-> ##[1:4] ack — whenever req is high, ack must go high within 1 to 4 cycles

The disable iff clause is essential for any concurrent assertion in a design with reset. Without it, the assertion will fire spuriously during reset when signals are transitioning to their initial state, flooding the log with false failures.

assert, assume, and cover

SVA provides three statement types that use the same property syntax but serve different purposes:

assert — The Design Must Satisfy This

assert property defines a rule the DUT must never violate. In simulation, a failure means a bug exists in the RTL. In formal verification, the tool attempts to prove the property holds for all possible inputs — or produces a counterexample showing when it fails.

// The arbiter must never grant two requesters simultaneously
assert property (@(posedge clk) disable iff (!rst_n)
    !(gnt[0] && gnt[1]))
    else $error("Simultaneous grant violation");

assume — The Stimulus Must Satisfy This

assume property constrains the inputs to the DUT. In simulation, assume has no effect — it is treated as a comment. In formal verification, the tool treats assume as a constraint on the input space: it only explores scenarios where the assumed property holds. This is how you tell a formal tool "the AXI master will never issue an unaligned transfer" — without needing to enumerate every valid input manually.

// Formal assumption: the input valid signal is never high for more than
// 8 consecutive cycles without a corresponding ready response
assume property (@(posedge clk) disable iff (!rst_n)
    $rose(valid) |-> ##[1:8] ready);

cover — This Scenario Must Occur

cover property is the inverse of assert: instead of checking that something never happens, it checks that something does happen at least once during simulation. A cover that never fires means the scenario it describes was never exercised — a coverage gap.

// Coverage: verify that back-to-back requests (req high two cycles in a row)
// actually occurred during this simulation run
cover property (@(posedge clk) disable iff (!rst_n)
    req ##1 req);

Use cover properties alongside assert properties. The assert checks correctness; the cover confirms the interesting scenario was actually stimulated. A passing assert on a scenario that never fired the cover means you have not actually tested that path.

Practical SVA Examples

The examples below show assertions for common design properties. For a full reference of SVA operators and sequence syntax, see SystemVerilog Assertions.

// ---------------------------------------------------------------
// 1. Handshake: valid must stay high until ready is seen
//    (AXI-style: once valid is asserted, it cannot be withdrawn)
// ---------------------------------------------------------------
property p_valid_stable;
    @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> valid;   // if valid with no ready, valid stays next cycle
endproperty
assert property (p_valid_stable)
    else $error("valid was deasserted before ready");

// ---------------------------------------------------------------
// 2. Mutual exclusion: read and write enables never simultaneously high
// ---------------------------------------------------------------
assert property (@(posedge clk) disable iff (!rst_n)
    !(rd_en && wr_en))
    else $error("Simultaneous rd_en and wr_en");

// ---------------------------------------------------------------
// 3. FIFO overflow: write enable must not be asserted when full
// ---------------------------------------------------------------
assert property (@(posedge clk) disable iff (!rst_n)
    !(wr_en && full))
    else $error("Write attempted to full FIFO");

// ---------------------------------------------------------------
// 4. Response latency: every request must get a response within 16 cycles
// ---------------------------------------------------------------
property p_latency;
    @(posedge clk) disable iff (!rst_n)
    req |-> ##[1:16] rsp;
endproperty
assert property (p_latency)
    else $error("Response timeout: no rsp within 16 cycles of req");

// ---------------------------------------------------------------
// 5. Cover: confirm that the maximum-latency case (exactly 16 cycles) was hit
// ---------------------------------------------------------------
cover property (@(posedge clk) disable iff (!rst_n)
    req ##16 rsp);

ABV in Simulation vs Formal Verification

The same SVA properties work in both simulation and formal verification — the syntax is shared, but the way the tool uses them differs fundamentally.

In Simulation

The simulator evaluates concurrent assertions on every clock edge throughout the run. An assertion fires when its condition is violated, generating an error with timestamp and signal context. Simulation-based ABV is sampled — it only checks the scenarios that the testbench stimulus actually exercises. Properties can pass for millions of cycles and still miss a bug if the triggering condition was never stimulated.

In Formal Verification

A formal tool treats the RTL and its assertions as a mathematical problem. It exhaustively searches all reachable states of the design — not just the states that random stimulus happens to visit — and either proves the assertion holds in every possible state, or produces a minimal counterexample showing exactly when it fails. This makes formal verification uniquely powerful for properties where the triggering condition is rare or hard to stimulate randomly.

The assume properties described earlier are particularly important for formal: they constrain the input space to legal behavior, preventing the formal tool from exploring impossible scenarios (such as protocol violations that the environment would never produce) that would otherwise trigger assertion failures.

Formal verification is most effective on focused blocks — arbiters, FIFOs, protocol checkers, reset logic, arithmetic units. Applying formal to a large SoC as a whole hits scalability limits quickly. The typical flow is: run formal on individual blocks during block-level verification, then use simulation ABV at subsystem and system level.

Where to Place Assertions

Assertions can be placed in three locations, each with different tradeoffs:

• Inside the RTL module: The assertion travels with the design through all verification stages — block level, subsystem level, and system level. It fires in every simulation environment that instantiates the block, including gate-level simulation. This is the preferred location for design-level invariants like FIFO overflow checks, FSM state encoding checks, and interface protocol rules.
• In a separate bind file: SystemVerilog's bind construct attaches assertions to a module without modifying the RTL source. This is useful when the RTL is a third-party IP block that cannot be modified, or when the team wants to keep verification logic strictly separate from design logic.
• In the testbench: Immediate assertions in testbench initial or always blocks check testbench-level conditions — driver compliance, protocol rule enforcement on stimulus, or scoreboard consistency checks.

Common Mistakes in ABV

// 1. Mutual exclusion: both grants never simultaneously high
assert property (@(posedge clk) disable iff (!rst_n)
    !(gnt[0] && gnt[1]))
    else $error("Simultaneous grant: gnt=%02b", gnt);

// 2. Grant implies request: a grant must only be issued to an active requester
assert property (@(posedge clk) disable iff (!rst_n)
    gnt[0] |-> req[0])
    else $error("Grant 0 issued without request 0");

assert property (@(posedge clk) disable iff (!rst_n)
    gnt[1] |-> req[1])
    else $error("Grant 1 issued without request 1");

// 3. Latency: if any request arrives while idle, a grant must appear within 2 cycles
property p_grant_latency;
    @(posedge clk) disable iff (!rst_n)
    ((req != 2'b00) && (gnt == 2'b00)) |-> ##[1:2] (gnt != 2'b00);
endproperty
assert property (p_grant_latency)
    else $error("Grant not issued within 2 cycles of request");

// Companion cover: confirm the maximum-latency case was actually exercised
cover property (@(posedge clk) disable iff (!rst_n)
    ((req != 2'b00) && (gnt == 2'b00)) ##2 (gnt != 2'b00));