From "I tried a million inputs" to "I proved all of them"
Imagine you build a bridge and a safety inspector drives a heavy truck across it a thousand times without it collapsing. Reassuring — but it is not a *proof* the bridge is safe. Maybe the one truckload you never tried, at the one temperature you never measured, is the one that brings it down. Every chapter of this track so far has been that truck: directed tests, constrained-random UVM stimulus, coverage dashboards. They drive enormous numbers of trucks across the bridge and watch for a collapse. That is dynamic verification, and it is indispensable. But it shares the truck's fatal limit — it can only ever exercise the inputs you actually generated.
Formal verification asks a completely different question. Instead of *running* the design, it builds a mathematical model of your logic and uses an automated reasoning engine — a SAT or SMT solver, the same family of tools that power theorem provers — to prove or disprove a statement about every possible input and every reachable state at once. There is no stimulus to write. You state a property — *this FIFO never overflows*, *grant is never asserted to two masters in the same cycle* — and the tool either returns a proof that it holds forever, or a concrete counterexample waveform showing exactly how to break it. One run, infinite trucks.
Assertions become theorems: formal property verification
Here is where rung 7 pays off. The SystemVerilog Assertions (SVA) you wrote to catch protocol violations in simulation are *exactly* the input formal needs. In simulation an assertion is a tripwire — it only fires if a running test happens to walk into it. Hand the same assertion to a formal property verification tool and it becomes a theorem to be proved: the solver searches the entire reachable state space for any trace that would make the assertion fail. Same line of code, vastly stronger guarantee.
A property splits into two flavours. A safety property says "something bad never happens" (`assert never two_grants`). A liveness property says "something good eventually happens" (`assert request |-> ##[1:$] grant` — every request is eventually granted). Safety properties are the bread and butter of property checking; liveness needs the tool to reason about unbounded time, which is harder but routine for modern engines. The art is writing properties that are both *meaningful* (they capture real intent) and *provable* (the tool can actually converge on them).
// A round-robin arbiter for 2 masters. Rung-7 assertions, now
// handed to a FORMAL tool as theorems over ALL inputs.
module arb (input logic clk, rst_n,
input logic req0, req1,
output logic gnt0, gnt1);
// ... RTL that picks a winner each cycle ...
endmodule
// --- Properties bound to the design (in a separate .sva file) ---
// SAFETY: never grant both masters in the same cycle (mutual exclusion)
ap_mutex: assert property (@(posedge clk) disable iff (!rst_n)
!(gnt0 && gnt1));
// SAFETY: never grant a master that didn't ask
ap_no_spurious: assert property (@(posedge clk) disable iff (!rst_n)
(gnt0 |-> req0) and (gnt1 |-> req1));
// LIVENESS: a held request is eventually granted (no starvation)
ap_no_starve: assert property (@(posedge clk) disable iff (!rst_n)
req0 |-> s_eventually gnt0);
// Tool result (illustrative):
// ap_mutex : PROVEN (holds for all reachable states)
// ap_no_spurious: PROVEN
// ap_no_starve : FAILED -> counterexample (CEX) of depth 6:
// cyc0 req0=1 req1=1 gnt0=0 gnt1=1 <- req1 always wins
// cyc1 req0=1 req1=1 gnt0=0 gnt1=1 because priority is
// ... fixed, not rotating
// => req0 starves forever. Fix the arbiter, not the property.How a solver searches time: bounded model checking
How does a tool prove a statement about *all* inputs without running any? The workhorse technique is bounded model checking (BMC). The idea is gloriously concrete: take your sequential circuit and unroll it in time like a flip-book. Copy the combinational logic once per clock cycle, wire each copy's flip-flop outputs into the next copy's inputs, and you get a giant purely-combinational formula representing every behaviour over the first *k* cycles. Add the negation of your property — "find a state where this *fails*" — and feed the whole thing to a SAT solver.
Unrolling the circuit for Bounded Model Checking (depth k):
state s0 --[comb logic]--> s1 --[comb logic]--> s2 -- ... --> sk
| in0 | in1 | in2
v v v
P(s0)? P(s1)? P(s2)? <- property
SAT query: s0 = reset_state
AND (transition s0->s1) AND (transition s1->s2) ...
AND ( NOT P(s0) OR NOT P(s1) OR ... OR NOT P(sk) )
SAT -> the solver found inputs in0..ink that reach !P => BUG (CEX)
UNSAT-> no failing trace exists within k cycles => safe so far
Push k deeper (k=20, 50, 200...) until either a CEX appears
or a PROOF technique (k-induction / IC3) closes it for ALL k.If the solver returns SAT, it literally found the input vector at each cycle that drives the circuit into a failing state — that *is* your counterexample. If it returns UNSAT at depth *k*, the property holds for at least *k* cycles. The crucial subtlety: a plain BMC pass that finds nothing only proves safety up to that bound. A bug might lurk at cycle *k+1*. To get an unbounded proof — "holds forever" — the tool layers on induction-style techniques (k-induction, interpolation, or the celebrated IC3/PDR algorithm) that establish the property is inductive: if it holds now, it must hold next cycle, for all states. When that closes, you have a full proof; until it does, you have a very strong *bounded* guarantee.
Drawing the fence: constraints and assumptions
There is a trap waiting for every formal newcomer. Run a property cold and the solver will gleefully feed your design *physically impossible* inputs — reset toggling every cycle, a bus protocol's request rising without a valid handshake, two illegal opcodes at once — and report a "failure" that could never happen in the real system. These are false counterexamples, and they come from the solver exploring inputs your environment would never produce. The fix is to *bound the proof space* with constraints and assumptions.
In SVA the keyword is `assume`. Where `assert` says *"the tool must prove this is always true,"* `assume` says *"the tool may take this for granted as a legal input."* Assumptions model the real environment: the bus protocol that surrounds your block, the reset sequence, the fact that an input is one-hot. Constrain too little and you drown in false failures. Constrain too much — an over-constraint — and you accidentally tell the solver to ignore the very scenario where the bug lives, getting a green PROVEN that means nothing. Calibrating this fence is the single most important formal skill.
// Without assumptions, the solver invents illegal stimulus and
// reports bogus failures. Assumptions pin the inputs to legal ones.
// ASSUME the environment holds reset, then releases it once:
am_reset_seq: assume property (@(posedge clk)
$fell(rst_n) |=> rst_n[*1:$]); // reset deasserts and stays high
// ASSUME the upstream master obeys the handshake:
am_valid_stable: assume property (@(posedge clk) disable iff(!rst_n)
(valid && !ready) |=> valid && $stable(data));
// ASSUME the opcode is always one of the legal encodings:
am_legal_op: assume property (@(posedge clk) disable iff(!rst_n)
op inside {ADD, SUB, LD, ST, NOP});
// Now ASSERT the real property; the proof is valid ONLY inside
// the world carved out by the assumptions above.
ap_result_correct: assert property (@(posedge clk) disable iff(!rst_n)
(op == ADD) |=> (result == $past(a) + $past(b)));
// RULE OF THUMB: assert = "prove this" assume = "trust this input"
// An over-tight assume can turn a real bug into a false PROVEN.
// => Always sanity-check assumptions (formal coverage / vacuity).Did synthesis lie? Equivalence checking
Formal has a second, entirely different superpower that almost every chip relies on. When you run logic synthesis, your human-readable RTL is mechanically transformed into a gate-level netlist — then optimized, retimed, had its clock gating inserted, scan chains stitched in, and buffers added during place-and-route. Each step is a tool rewriting your logic for area, timing, and power. How do you know the netlist that goes to the foundry still computes the *same function* as the RTL you so carefully verified? You cannot re-run your entire UVM suite on the gate netlist — it would take weeks. Instead you use equivalence checking.
An equivalence checker — strictly, a *combinational* equivalence checker (CEC), the everyday kind — takes two designs, identifies their matching state elements and primary I/O (the key points), then formally proves that for *every* possible input, the logic cone driving each output is Boolean-identical between RTL and netlist. It does not simulate; it uses the same SAT/BSP engines to prove equivalence outright. Because it only compares combinational logic between registers, it sidesteps the state-explosion problem and scales to designs with hundreds of millions of gates — which is exactly why it runs on essentially every block at every synthesis and place-and-route handoff.
Equivalence Checking: golden RTL vs. synthesized netlist
RTL (golden) Gate netlist (revised)
┌────────────────────┐ ┌──────────────────────────┐
in ─►│ a&b | c │─► out in ─►│ NAND-NAND remap, buffers,│─► out
│ (behavioural) │ │ clock-gating, scan FFs │
┌─►ff │ │ ┌─►ff │ (logically equal?) │
└────────────────────┘ └──────────────────────────┘
│ │
└──────── match key points ──────┘
For each output cone: prove RTL(out) XOR NETLIST(out) == 0
for ALL input combinations.
PASS : every key point is logically identical -> synthesis safe
FAIL : a miscompare point + input pattern that distinguishes them
(e.g. a wrong don't-care optimization, dropped reset, or a
mis-set retiming option) -> netlist does NOT equal RTL.Two nets, one signoff: formal and dynamic together
It is tempting to crown formal as the winner — it *proves*, after all. Resist it. Formal and dynamic verification are not rivals; they are two nets stretched across different gaps, and a real signoff needs both. Formal is exhaustive but local: it excels on bounded, control-heavy properties and on equivalence, yet it chokes on deep datapaths and cannot easily express "the JPEG decoder produces a visually correct image." Simulation and UVM are shallow but global: they run the *whole* SoC with real software, real models, and full system scenarios, but only on the stimulus you generate. The frontier of verification is knowing which gap each net was built to cover.
- Reach for formal first on control logic where a bug is catastrophic and the state space is tractable: arbiters, FSMs, FIFOs, register-access maps, deadlock and bus-protocol compliance. Here exhaustive proof beats any amount of random simulation.
- Lean on simulation/UVM for end-to-end behaviour, performance, embedded software bring-up, mixed-signal, and wide datapaths — anything where running the real system matters more than proving a single property.
- Let assertions bridge them. The same SVA runs as a tripwire in UVM *and* as a theorem in formal — write once, get both coverage in sim and proof in formal.
- Run equivalence checking at every handoff from RTL down to the layout database — it is non-negotiable, lightweight, and catches the class of bug that simulation-on-RTL can never see because it lives in the synthesis/PnR transformation itself.
And that closes the track. You started by writing testbenches and watching waveforms; you learned to randomize stimulus, measure coverage, structure a UVM environment, and pin behaviour down with assertions. Now those assertions have become mathematical theorems, your synthesis is provably faithful, and you can articulate *why* a mature project pours millions into both a regression farm and a formal team. Verification is not about running more tests — it is about building a justified, layered argument that the chip is correct before a single wafer is etched.