Formal Property Verification

Everything in this module so far — the mightiest UVM bench, a million seeds, closed coverage — shares one quiet limitation: simulation samples. Each test walks one path through the design's possible behaviours; a green regression says "no failure on the paths we happened to walk". Formal property verification makes a different kind of statement entirely: a tool explores every reachable state of the design and returns a mathematical verdict — the property holds in all of them, or here is an input sequence that breaks it. Not "we didn't find a bug"; "there is no bug of this kind to find". This lesson is about what that promise really means, where it is achievable, and where it quietly runs out.

Model checking: the state space as a map

The design is a state machine: its flip-flops define a state, and each clock edge moves it to a successor state that depends on the inputs. A model checker treats this as a graph problem. Start at the reset state; follow every possible input, to every successor, and theirs, and theirs — until no new state appears. That fixed set is the reachable states, and the property (the very same SVA you wrote in the assertions lesson — formal reuses them verbatim) must hold at every one of them:

property no_double_grant; // same language, new verdict @(posedge clk) disable iff (!rst_n) !(g0 && g1); endproperty assert property (no_double_grant); // simulation: "held in every cycle we happened to run" // formal: "PROVEN — holds in every reachable state" // or "cex at depth 2: r0=1, r1=1, …" (a concrete failing trace)

Note the word reachable. A design with n flip-flops has 2^n possible states, but reset and the update logic may make most of them impossible to ever enter — and the checker rightly ignores those, or it would report failures no real silicon could exhibit.

The explosion, and where formal shines

The catch has a name: state-space explosion. Every extra flip-flop doubles the state space — n flops make 2^n states — and exponentials do not negotiate:

Around 55 flip-flops, the states outnumber what a year of brute-force simulation could even touch — and a single 64-bit datapath register blows past that on its own. This is why formal tools do not enumerate states one by one (they reason about huge sets of states symbolically), and it is why formal has a home turf: control logic. Arbiters, FIFO pointers, handshake protocols, state machines — tens of flip-flops of dense, corner-case-riddled logic where bugs love to hide and the reachable space is small enough to conquer. A 64-bit multiplier's datapath, by contrast, is simulation's job (or specialised equivalence tricks). The craft of formal is carving out the control kernel and proving it watertight.

When a full proof is out of reach, tools fall back to bounded model checking (BMC): prove the property holds for every input sequence of length up to k — "no violation within 20 cycles of reset". That is not a proof for cycle 21; it is a depth-k guarantee, and in practice a superb bug-finder, because most control bugs have short minimal traces. Reports read "proven" (unbounded, done) or "no cex to depth k" (keep the asterisk).

Be the model checker

For a small design you can do exhaustive reachability by hand — breadth-first search over states, trying every input at every step. Here is a two-requester round-robin arbiter (3 flops: two grants plus a fairness bit) and the property no two grants ever simultaneous — first a correct design, then one whose arbitration was "simplified" away:

// ── Exhaustive BFS over the reachable states = a tiny model checker. ── type S = { g0: number; g1: number; last: number }; const key = (s: S) => `${s.g0}${s.g1}${s.last}`; function check(name: string, next: (s: S, r0: number, r1: number) => S): void { const reset: S = { g0: 0, g1: 0, last: 0 }; const seen = new Map<string, { prev: string | null; via: string }>(); seen.set(key(reset), { prev: null, via: "reset" }); const frontier: S[] = [reset]; let bad: string | null = null; while (frontier.length && !bad) { const s = frontier.shift()!; for (const r0 of [0, 1]) for (const r1 of [0, 1]) { // EVERY input, not a sample const n = next(s, r0, r1); if (seen.has(key(n))) continue; seen.set(key(n), { prev: key(s), via: `r0=${r0} r1=${r1}` }); if (n.g0 && n.g1) { bad = key(n); break; } // property violated! frontier.push(n); } } console.log(`${name}: ${seen.size} reachable states (of 8 possible)`); if (!bad) { console.log(" PROVEN: g0 and g1 never high together, in ANY reachable state"); return; } const trace: string[] = []; // walk predecessors back to reset for (let k: string | null = bad; k; k = seen.get(k)!.prev) trace.unshift(`${seen.get(k)!.via} -> g0=${k[0]} g1=${k[1]} last=${k[2]}`); console.log(" COUNTEREXAMPLE (shortest failing trace):"); for (const line of trace) console.log(" " + line); } // Round-robin: on contention, grant whoever did NOT go last. const arbiter = (s: S, r0: number, r1: number): S => { if (r0 && r1) return s.last === 0 ? { g0: 0, g1: 1, last: 1 } : { g0: 1, g1: 0, last: 0 }; return { g0: r0, g1: r1, last: r1 ? 1 : r0 ? 0 : s.last }; }; // "Simplified" version: each grant just follows its request. What could go wrong? const buggy = (s: S, r0: number, r1: number): S => ({ g0: r0, g1: r1, last: s.last }); check("round-robin arbiter", arbiter); check("buggy arbiter ", buggy);

Two things to savour. The proof covered only 4 reachable states, not all 8 — reachability did real work. And the failure comes back not as a percentage or a red bar but as a counterexample: the exact, minimal input sequence — reset, then both request — driving the design into the bad state. Real formal tools hand you this as a waveform; debugging a formal counterexample is often easier than debugging a random-simulation failure, because the tool has already minimised the story for you. The counterexample is the payoff.

Two more places formal earns its keep

Equivalence checking. After synthesis turns your RTL into a gate-level netlist, how does anyone know the tool preserved the design's meaning? Not by re-running the regression on gates (weeks of runtime) — by formally proving that RTL and netlist compute identical next-state and output functions, register by register. Every tape-out on Earth rests on this proof; it is why the industry gets to trust synthesis and never simulate the netlist exhaustively.

Assume–guarantee at interfaces. A block in isolation sees inputs its real neighbours could never send, so naive formal drowns in false alarms. The fix: assume properties about the inputs (legal protocol only), and prove your properties under those assumptions. The elegant part — when the neighbouring block is verified, your assumptions become its proof obligations (its guarantees), and the proofs compose across the interface like a contract with matching signatures. Divide, constrain, and conquer.

simulation samples behaviours; model checking explores all reachable states and returns proven or a counterexample — the exact minimal failing trace;
n flip-flops → 2^n possible states: the state-space explosion confines full proofs to control logic (arbiters, FIFOs, handshakes), not wide datapaths;
bounded model checking proves "no violation within k cycles of reset" — a depth-limited guarantee and a superb bug-finder;
equivalence checking proves RTL ≡ synthesized netlist — the reason the industry trusts synthesis;
assume–guarantee: constrain inputs to legal behaviour; your assumptions become the neighbour's proof obligations, so proofs compose at interfaces.

It cannot — one at a time. The 1980s breakthrough (Clarke, Emerson and Sifakis, later the 2007 Turing Award) was symbolic model checking: represent an astronomically large set of states as a compact formula — first as binary decision diagrams, later as SAT problems — and step whole sets through the design's logic at once. "All states where the FIFO is empty and no grant is high" might be a trillion states and a twelve-node data structure. The state count stops mattering; the structure of the logic is what the tool pays for. That is also the honest reading of formal's limits: on tangly control logic the formulas stay small and proofs fly; on multipliers they balloon, which is why your formal testplan says "arbiter: prove" and "datapath: simulate" — and why the modern SAT-solver renaissance keeps moving that boundary outward.

Formal's guarantee is airtight about exactly one thing: the listed properties hold in every reachable state. Weak properties, weak guarantee: prove three easy assertions about a cache controller and the marketing sentence "formally verified" is true while the eviction logic ships broken. Worse is the vacuous proof: req |-> ##2 grant is triumphantly "proven" on a design where an over-tight input assumption means req can never rise — the implication held because it was never tested. (An assumption contradiction can even prove false.) Good tools report vacuity and covered preconditions; good engineers read those reports, and ask the same question this module keeps asking of coverage and scoreboards alike: not "did the check pass?" but "could this check have failed?" Formal moves the risk from "did we try the scenario?" to "did we state the requirement?" — the burden of imagination never goes away, it just changes address.