Assertions and SVA

A specification that lives in a Word document is a rumour: nobody executes it, nobody notices when the design drifts away from it. SystemVerilog's answer is to make the spec executable: assertions are statements of intent — "this must always hold" — written into the code, checked automatically on every cycle of every simulation you ever run. The dialect for writing them, SystemVerilog Assertions (SVA), is a little temporal-logic language for saying things like "every request is granted within three cycles" — sentences about time, which ordinary boolean expressions cannot utter. Learn to write them well and your design carries its own spec around, machine-checked, forever.

Immediate assertions: sanity checks in the bench

The simple kind first. An immediate assertion is a boolean check at a point in procedural code — a testbench's way of saying "at this moment, this had better be true":

// In a testbench, right after driving inputs and waiting: assert (sum === a + b) else $error("adder wrong: %0d + %0d gave %0d", a, b, sum);

This is the self-checking idea from last lesson wearing its official uniform: the assert … else $error pattern is how checks are spelled in professional benches (note ===, the four-valued equality that refuses to call x a match). Useful — but it only checks one instant. The interesting bugs live across instants.

Concurrent assertions: properties that live in time

A concurrent assertion is evaluated at every clock edge, watching signals unfold over cycles. Its vocabulary:

##N — "N cycles later"; ##[1:3] — "between 1 and 3 cycles later" (a window);
|-> — implication: "whenever the left side (the antecedent) occurs, the right side (the consequent) must follow", checked starting the same cycle;
disable iff (…) — "don't check while this holds" (universally: during reset).

The canonical example — an arbiter that must answer requests promptly:

property req_gets_grant; @(posedge clk) disable iff (!rst_n) req |-> ##[1:3] grant; // every request: a grant within 1 to 3 cycles endproperty assert property (req_gets_grant); // No grant may appear out of thin air: assert property (@(posedge clk) grant |-> $past(req)); // A FIFO must never be pushed while full: assert property (@(posedge clk) disable iff (!rst_n) !(push && full));

Read the first one aloud: at every clock edge (except during reset), if req is high, then at 1, 2 or 3 edges later grant must be high at least once. Three lines of spec-English, now machine-checked on every run. The other two show the pattern's range: a backward-looking rule ($past reads last cycle's value) and a pure invariant with no temporal window at all — "never both".

The property, on a waveform

Every req pulse starts a fresh attempt of the property, with its own window counted from its own cycle. A busy trace has many attempts in flight at once — the simulator tracks them all, and one late grant fails only the attempts whose windows it missed.

Be the assertion engine

An SVA checker is a simple machine: scan the trace; at each antecedent, open a window; report any window that closes unsatisfied. Here it is in forty lines, run against a clean trace and a buggy one:

// One recorded cycle of the DUT's signals. interface Cyc { req: number; grant: number } // Check: req |-> ##[min:max] grant over a whole trace. function check(name: string, trace: Cyc[], min: number, max: number): void { let violations = 0, attempts = 0; trace.forEach((c, t) => { if (!c.req) return; attempts++; const win = trace.slice(t + min, t + max + 1); // the consequent's window const hit = win.findIndex((w) => w.grant === 1); if (hit < 0) { violations++; console.log(` VIOLATION: req at cycle ${t}, no grant in cycles ${t + min}..${t + max}`); } else { console.log(` ok: req at cycle ${t} → grant at cycle ${t + min + hit}`); } }); if (attempts === 0) console.log(" no req ever fired — property passed VACUOUSLY (it checked nothing!)"); console.log(`${name}: ${attempts} attempts, ${violations} violations\n`); } const r = (req: number, grant: number): Cyc => ({ req, grant }); // A well-behaved arbiter: each req answered 2 cycles later. const goodTrace = [r(0,0), r(1,0), r(0,0), r(1,1), r(0,0), r(1,1), r(0,0), r(0,1)]; check("good trace", goodTrace, 1, 3); // A lazy arbiter: the second req's grant arrives 4 cycles late. const badTrace = [r(0,0), r(1,0), r(0,1), r(1,0), r(0,0), r(0,0), r(0,0), r(0,1)]; check("bad trace", badTrace, 1, 3); // A trace where req never fires at all: check("idle trace", [r(0,0), r(0,0), r(0,0), r(0,0)], 1, 3);

The third run is the quiet trap: no antecedent, no check. The property "passed", having examined nothing — a vacuous pass. Assertion tools count and report vacuity for exactly this reason; a green assertion that never triggered is a smoke alarm with no battery.

Assertions as embedded documentation

Assertions do not only live in benches. Designers embed them inside the RTL itself — next to the FIFO, an assertion that it never overflows; next to the FSM, that its one-hot state register stays one-hot; at a module boundary, the interface's handshake rules. Embedded assertions are the best documentation in the building: unlike comments, they cannot go stale silently, because every simulation re-checks them. Two siblings complete the family: assume declares what the environment promises (constraining legal inputs), and cover asks "did this scenario ever actually happen?" — a question the coverage lesson turns into a discipline. And the same properties get a second, more spectacular life in formal verification, where a tool proves them instead of sampling them.

immediate assertions check a boolean at a point in procedural code; concurrent assertions check properties at every clock edge;
vocabulary: ##N / ##[m:n] delays, |-> implication (antecedent → consequent), disable iff for reset;
each antecedent occurrence starts its own attempt with its own window;
an attempt-free run is a vacuous pass — green, but it checked nothing;
assert claims, assume constrains the environment, cover asks "did it happen?"; embed assertions in the RTL as living spec.

From philosophy, of all places. Temporal logic — a formal calculus for "always", "eventually", "until" — was developed by the logician Arthur Prior in the 1950s to analyse statements about time in language and metaphysics. In 1977 Amir Pnueli realised it was exactly the right mathematics for reasoning about programs that never terminate — operating systems, protocols, and (it turned out) hardware, whose whole life is one endless loop of cycles. That insight won Pnueli the Turing Award, and its industrial descendants are the property languages of chip design: SVA and its cousin PSL are temporal logic in engineer's clothing. When you write req |-> ##[1:3] grant, you are using a notation whose family tree passes through modal logic seminars — one of the cleanest pipelines from pure philosophy to fabbed silicon in all of engineering.

SVA has two implication arrows, one character apart, one clock cycle apart. |-> (overlapping) starts checking the consequent in the same cycle as the antecedent; |=> (non-overlapping) starts one cycle later — it is exactly |-> ##1. So req |-> grant demands the grant this very cycle, while req |=> grant demands it next cycle. Mix them up and your assertion checks a different spec than the one in your head: an off-by-one that either fails good designs (the assertion is one cycle too eager) or — far worse — passes bad ones (one cycle too lenient, quietly blessing late grants). This is the classic SVA bug, and the defence is ritual: when writing any implication, say the sentence aloud with cycle numbers ("req at cycle T, so grant must be high at cycle T+…?") and pick the arrow that matches. Then check it against a hand-drawn waveform — two minutes that regularly save two weeks.