Assertions & Assertion-Based Verification (SVA)

The bug that hides 10,000 cycles downstream

Imagine a bank where the only way to detect fraud is to wait until the end of the year, total every account, and check whether the books balance. If they don't, *something* went wrong — but which transaction, on which day, at which branch? You would spend weeks unwinding the ledger. That is exactly how a traditional testbench catches bugs: it drives stimulus in, lets the design run for thousands of clock cycles, and finally compares the output against a reference model. When the mismatch appears at cycle 84,217, the actual mistake — a FIFO that was written while full — may have happened at cycle 31,002. The output check is the *symptom*; the root cause is buried 53,000 cycles upstream.

An assertion is a continuously-watching auditor standing *at* the branch, *at* the teller's window. The moment someone tries to write a full FIFO, the auditor fires — at cycle 31,002, on the exact signal, in the exact module. You debug at the source, not at the symptom. This is the entire promise of the technique, and it is why a SystemVerilog Assertion (SVA) is one of the highest-leverage things you can add to an RTL design.

Two flavours: immediate vs concurrent

SVA comes in two kinds, and confusing them is the most common beginner mistake. An immediate assertion is just an `if`-test that lives in procedural code. It fires the instant simulation reaches it, like a friend who interrupts you mid-sentence. It has no notion of clocks or time — it checks a condition *right now*. Use it for sanity checks inside an `always` block or a piece of testbench code: 'this index must be in range', 'this state is not X right this instant'.

// IMMEDIATE — runs inside procedural code, no clock involved
always @(posedge clk) begin
  if (wr_en) begin
    assert (!full)
      else $error("write to FULL fifo at addr %0d", wr_ptr);
  end
end

// CONCURRENT — a standalone temporal contract, sampled every clock
assert property (@(posedge clk) wr_en |-> !full);
//        \____ property ____/    \__ antecedent _/  \_ consequent _/

The same rule — 'never write a full FIFO' — as an immediate assertion (procedural) and a concurrent assertion (temporal contract).

A concurrent assertion is the real star. It is a standalone, declarative statement that lives outside procedural code and is evaluated on a clock edge, comparing values *across time*. The clue is the keyword `property` and a clocking event like `@(posedge clk)`. Concurrent assertions can say things no `if`-statement can: 'a request must be granted within 3 cycles', 'after `start` rises, `done` must eventually rise and `error` must stay low until then'. They reason about sequences of events, which is precisely what protocols are made of.

Sequences and properties: a grammar for time

Concurrent assertions are built from two layers, like sentences built from phrases. A sequence is a phrase — a pattern of signal values stretched over consecutive clock cycles. A property is the full sentence — it combines sequences with implication and logical operators to state a complete rule. You write the phrases, then assemble them into the contract.

// ## DELAY: ##N means "N clocks later"; ##[1:3] is a window
sequence req_then_gnt;
  req ##[1:3] gnt;        // gnt comes 1 to 3 cycles after req
endsequence

// ## REPETITION: [*N] = N times; [->N] = the N-th occurrence
sequence stable_burst;
  valid [*4];            // valid held high for 4 consecutive cycles
endsequence

// ## IMPLICATION builds a property from an antecedent and a consequent
property handshake;
  @(posedge clk) disable iff (rst)
    req |-> ##[1:3] gnt; // if req, THEN gnt within 1..3 cycles
endproperty

assert property (handshake);   // turn the contract into a live check

Sequences describe patterns over time; a property wraps them in an implication; assert makes it a runtime check.

The heart of almost every property is the implication operator. `a |-> b` reads 'if `a` (the antecedent) matches, then `b` (the consequent) must hold'. The overlapping form `|->` checks the consequent starting on the *same* cycle the antecedent finishes; the non-overlapping form `|=>` starts checking *one cycle later*. The beauty of implication is vacuity: when the antecedent never happens, the property is trivially true and stays silent. A grant-within-3-cycles rule simply does nothing on cycles where there was no request — exactly what you want.

assert · assume · cover — the same property, three jobs

Here is the elegant part that pays off in rung 8. Once you have written a property, you can *direct* it three different ways with three keywords — and the property text never changes. This is the bridge between simulation and formal.

assert — *check it*. The tool must prove (in formal) or never observe a violation (in simulation) of this property. This is your obligation: 'I claim this is always true; catch me if it isn't.'
assume — *trust it*. This property describes a constraint on the inputs — a promise about how the environment behaves. In simulation it is a check; in formal it *constrains the legal input space* so the prover only explores realistic scenarios. 'The bus master never sends two requests without waiting for a grant.'
cover — *measure it*. This asks 'did this interesting scenario ever actually happen?' It never fails — it succeeds or it never triggers. A `cover` on `req ##[1:3] gnt` tells you whether your stimulus ever even exercised the handshake you so carefully checked.

// One property text → three uses
property p_no_overflow;
  @(posedge clk) disable iff (rst) wr_en |-> !full;
endproperty

assert property (p_no_overflow);   // DUT must obey this
assume property (p_bus_legal);     // environment promises this (constrains inputs)
cover  property (p_no_overflow);   // did we ever even write near-full? did the case occur?

assert/assume/cover are three verbs over the same noun. assert = obligation, assume = environment contract, cover = was it exercised.

Assertion-based verification as a methodology

Sprinkling a few asserts is a trick. Assertion-based verification (ABV) is a *methodology* — a deliberate practice of capturing design intent as a dense web of assertions, written early and living in the code forever. The payoff compounds. Assertions are written once and check on *every* test in your regression, around the clock, with zero extra stimulus. They turn a passive testbench that only checks the output into thousands of internal monitors checking every protocol, every FIFO, every handshake, on every cycle.

There are two homes for these assertions. White-box assertions live inside the RTL, written by the designer who knows that `wr_ptr` should never pass `rd_ptr` — they catch internal mistakes the moment they occur. Black-box (interface) assertions sit on module boundaries and on standard protocols. Vendors ship pre-packaged assertion IP — for example a complete AMBA AXI checker — so you bind a hundred hand-verified protocol rules onto your interface without writing a single one. Many designers reuse the very same checks the UVM monitor relies on to flag illegal transactions.

Did the watchdog ever wake up? Assertion coverage

Here is the trap that catches even strong teams. A property that *never fails* feels like good news — but a property whose antecedent never matches is also a property that never *did anything*. If `req` was never asserted in any of your tests, then `req |-> gnt` passed on every run while proving absolutely nothing. A green dashboard of all-passing assertions can be entirely hollow.

This is exactly the coverage thinking from rung 6, now aimed at the checks themselves. Assertion coverage measures whether each assertion was genuinely *exercised* — specifically, whether its antecedent ever matched so the consequent was actually tested. It is the natural partner to the functional coverage you already track on the design, and to the structural code coverage of the RTL. Coverage of the design tells you *what the DUT did*; assertion coverage tells you *whether your checks watched it*.

ASSERTION REPORT                attempts  pass  fail  vacuous
--------------------------------------------------------------
p_no_overflow  (wr_en |-> !full)    8421   8421     0        0   <- good: real checks happened
p_handshake    (req   |-> gnt)         0      0     0        0   <- ALARM: never exercised!
p_no_x_on_bus  (!$isunknown(data))  152k   152k     0      14k   <- 14k vacuous: antecedent rarely true

An assertion-coverage report. Zero attempts on p_handshake means a hole in the stimulus, not a healthy design — the check was asleep.

And here is the elegant bridge to rung 8. The very same property you wrote for simulation is the input a property-checking tool reads to attempt a mathematical proof — exhaustively, over *every* legal input, with no stimulus at all. In simulation, an assertion is only as good as the tests that trip it; in formal, the tool tries every path itself. Your `assume` statements become the formal constraints, your `assert` statements become the proof obligations, and your `cover` statements become reachability goals. You will have already written 90% of your formal setup just by practising disciplined ABV.