Formal verification

A test runs a design on some inputs and checks the answers. However many tests there are, they only cover the inputs they try. Formal verification checks a claim for every input there could be, and either proves it or gives an input that breaks it. Chip makers rely on it, and it isn’t only for hardware: the same tools check software too. Every proof on this page runs here, with the SAT solver built into Yosys.

1 · Why testing isn’t enough

An 8-bit adder has two 8-bit inputs: 65,536 pairs, and a computer can try every one in a blink. A 32-bit adder has 2⁶⁴ pairs. At a billion tests a second, trying them all would take nearly 600 years. And an adder is the easy case: its answer depends only on its inputs. A design with memory gives answers that depend on everything that happened before, so the number of situations to test has no end.

Bugs hide in the corners tests don’t reach. In 1994, Intel’s Pentium was found to divide some numbers wrongly, from a few missing entries in a table that the chip’s tests had never exercised. Replacing the chips cost Intel $475 million, and formal verification has been part of how processors are checked ever since.

2 · Asking a solver instead

The claim to check is written into the design as an assertion: assert (sum == a + b); says “this is always true”. (assert comes from SystemVerilog, the larger language built on Verilog, which most Verilog tools also read.)

Then, instead of trying inputs, the tool turns the circuit and the assertion into one big Boolean formula, and asks a SAT solver (from satisfiability) a question: is there any setting of the inputs that makes the assertion false? A SAT solver is a program that answers exactly that kind of question, about formulas with thousands or millions of variables. In general the problem is hard (no method is known that’s always fast), but on circuits like these, modern solvers usually answer in moments. If the answer is no, there is no input that breaks it, and the claim is proven. If yes, the solver gives the input: a counterexample.

A 32-bit ripple-carry adder, built column by column from full adders (the generate loop writes out 32 columns), with one mistake: column 5 forgets its carry in. The assertion compares it with Verilog’s own +. The solver finds a counterexample in a moment: a and b (in hex) for which the sum comes out wrong. Switch to the fixed adder: proven, for all 2⁶⁴ pairs, without trying them.

3 · Circuits with memory: bounded model checking

For a design with flip-flops, a counterexample is a story: a sequence of inputs, one per clock cycle, that leads from the start to a state where an assertion is false. Bounded model checking looks for one of up to N cycles: it writes out N copies of the circuit side by side, each feeding its flip-flops’ next values into the next copy, and asks the solver whether any choice of inputs, in any of the N cycles, breaks an assertion.

The solver isn’t guessing or trying cases in turn. It reasons about every possible sequence of inputs at once, and the counterexample it finds is often one nobody would have thought to test.

A FIFO, a queue of up to 4 bytes, with a mistake: it accepts a push when it’s already full. The assertion says it never holds more than 4. The solver chooses push, pop and din freely each cycle, and finds the shortest way to break it: push five times. The trace is a waveform of that run, with the last step the one that fails. Fix it in the editor (push && !full) and click Prove, or switch to the fixed FIFO: proven.

4 · Proof by induction

Bounded model checking only looks N cycles ahead. A bug that takes a thousand cycles to show would need N of a thousand. To cover every cycle, there’s induction, as in mathematics: show the claim is true at the start, then show that whenever it’s true, it stays true after one more cycle. Then it’s true forever.

The second half is the tricky part. The solver is asked: is there any state where the assertions hold, from which one cycle leads to a state where they don’t? Any state at all, including ones the design could never reach from the start. If such a state exists, induction fails, even when the claim is really true.

The cure is to look further back. k-induction asks whether k good states in a row can be followed by a bad one, which is harder for an unreachable state to manage. Yosys, like most tools, only counts runs where all k states are different, following a method from 2003 by Niklas Eén and Niklas Sörensson. A run that just waits in an unreachable state repeats itself, so it doesn’t count.

The counter counts 0 to 9, so q never reaches 15. With steps at 1 it isn’t proven: q = 14 is a state where the assertion holds, and one cycle later q is 15. The counter never gets to 14, but induction doesn’t know that. Raise steps one at a time: the trace starts further back, at 13, then 12, until at 6 steps it would have to start below 10 (where the counter wraps instead), and the proof goes through. Or make a stronger claim, q is never over 9: true of every state it allows, so induction proves it in one step.

That’s the everyday art of formal verification: when induction fails on a true claim, add the other facts the design keeps true (assertions about its other registers), until together they’re strong enough to carry each other.

5 · A claim that matters

The door lock from Clocked circuits should open only after 2, 7, 1. A test can press a few sequences of keys; a proof covers every sequence there is, of any length.

To state the claim, the design keeps a record of the last three keys pressed (k1 the latest), separate from the lock’s own logic, and asserts that whenever the lock is open, those were 2, 7, 1. The solver may press any keys, at any time. Proven, with induction over 4 steps. Set steps to 3: not proven, from a state the lock can never be in (it has heard a 2, but the last key pressed was something else).

6 · In practice

The proofs here use Yosys’s own solver. Larger projects use SymbiYosys, which runs Yosys with faster solvers (including SMT solvers such as Z3 and Bitwuzla, which reason about whole numbers as well as bits), and supports assume (limit the inputs to ones that are allowed, such as a valid instruction) and cover (find a run that reaches some situation, to check the design can do something at all).

For software people: this is the same idea as property-based testing, where a test states a property and the tool tries many inputs, except that the solver covers all of them. It’s used on software too. CBMC checks C programs by bounded model checking, the seL4 operating-system kernel was proven correct in 2009, and Amazon Web Services uses formal methods to check the designs of its distributed systems.

Summary

Tests cover the inputs they try; formal verification covers every input, and every sequence of inputs.
Assertions state the claims. A SAT solver looks for inputs that make one false: if there are none, the claim is proven; if there are, it gives a counterexample.
Bounded model checking looks for a counterexample within N cycles of the start, and finds the shortest.
Induction proves a claim for every cycle, but can fail on a true claim from a state the design never reaches. Look further back (k-induction), or strengthen the claim.