Verifying a CPU

Verifying a CPU means finding out whether it really implements its instruction set, in every combination of instructions, timing and memory behavior. A bug that reaches silicon can cost millions of dollars and months of delay, and famous ones have forced recalls. Yet the space of possible behavior is unimaginably large, so no single test method is enough. This article explains how CPU verification works: reference models, test suites, random instruction generators, formal proofs and real software, with real bugs of the kinds they find.

11 min read | Intermediate

What You'll Learn

• Explain why CPU verification is so hard
• Describe how a reference model checks a running core
• Compare directed tests, random generators and formal methods
• Use coverage to decide when verification is done

Why It Is Hard

A CPU has a huge number of states. A 32-bit core with 31 registers has more register states alone than anyone could ever enumerate, and bugs often need a particular sequence of instructions, with particular timing from memory. In 1994, a missing entry in a lookup table in a famous desktop processor's divide unit gave wrong answers in rare cases. It cost the company hundreds of millions of dollars. Bugs like that are why verification often takes more engineers than design does.

The goal is to find bugs, not to prove that none exist. Teams combine several methods, each strong where the others are weak:

The Reference Model

The basic question is how to tell whether a test passed. A hand-written expected result works for small tests, but not for millions of random ones. The answer is a reference model: a simple, trusted software simulator of the instruction set, with no pipeline, that runs each instruction in turn. Spike is the standard for RISC-V, and others exist.

A simulation runs the RTL and the model side by side. Each time the RTL commits an instruction, the checker compares the PC, the destination register's value, and any memory write with what the model says. This is lock-step comparison, or commit-trace checking. A mismatch points to the exact instruction where things first went wrong, often thousands of cycles before the program itself would have crashed. Interfaces such as RVFI and RVVI, which expose committed instructions from a core, exist to make this easy.

The approach depends on the model being independent of the design. Both are written from the specification, so a bug would have to be made twice in the same way to slip through. When they disagree, someone must read the specification and decide who is wrong. Sometimes it's the model.

Some things aren't fixed by the ISA, such as the exact cycle of an interrupt or the value of a cycle counter. Checkers must allow for these, usually by telling the model when an interrupt was taken, in the RTL's own timing.

Directed Tests and Suites

Directed tests are written by hand to hit a specific case: each instruction, with extreme values; each hazard, such as a load followed by its use; each exception. They're easy to debug, and they catch the obvious problems quickly. In the bring-up of a new design, they are the first thing to run.

ISA compliance suites, such as the riscv-arch-test suite, check that each instruction does what the standard says, which is needed to claim RISC-V compatibility. They test the architecture, so passing doesn't mean that a pipeline has no bugs. Many pipeline bugs appear only with particular timing, and these suites don't try to create that.

A small but very effective trick is a matrix of runs. Run the same set of programs across every combination of configuration: forwarding on and off, memory latency of 0, 1, 2 and 4 extra cycles. A compare with a host-compiled expected result then gives a cheap regression. One real example caught a bug in which a forwarded value was lost while the pipeline was frozen, because of slow memory. Four of six programs failed at just one extra cycle of latency, and all had passed with instant memory.

Random Instruction Generators

Humans write tests for the cases they think of. Bugs are often in cases they don't think of. A random instruction generator, such as the open-source riscv-dv, produces long programs of legal instructions, with biased random choices: many branches, many dependent instructions, nested loops, tricky addresses. The RTL and the reference model both run it, and any difference is a bug.

Pure randomness is not enough, because the interesting cases are rare. Good generators are constrained. They use just a few registers, so that dependences occur often. They place data so that accesses cross cache lines and pages. They insert interrupts at random times. And the environment randomizes memory delays and bus errors, so that every internal timing can occur.

The strength of random testing is that it finds combinations nobody imagined. Its weakness is debugging: a failure in a 100,000-instruction program must be reduced, by removing instructions, until a small program still shows it.

Formal Verification

Formal verification proves properties mathematically, for every possible input, rather than trying examples. A tool is given an assertion, such as "a stalled instruction never loses its operands", and it explores all reachable states to prove it, or else it produces a short trace that breaks it. These traces are often the shortest possible example of the bug, which makes them very easy to debug.

It works well on small, intricate blocks: arbiters, FIFOs, the forwarding and hazard logic, a coherence protocol, bus interfaces. It has limits with size. A whole processor has too many states, although methods exist for proving each instruction correct in the full pipeline, one at a time, such as riscv-formal. See the Formal Verification tutorial for how these tools work.

Assertions are worth writing anyway, even without a formal tool. A statement in the RTL such as "the FIFO never overflows" is checked in every simulation, and it catches a bug at the moment it happens rather than much later, when a wrong value finally reaches a register.

Real Software

Finally, run real software: boot an operating system, run compilers, run benchmarks. This covers behaviors that no one thought to generate, like long sequences of context switches and page faults. It takes billions of cycles, so it can't be done in RTL simulation. Teams use FPGA prototypes and emulators, which run the design thousands of times faster. Booting Linux on the design before tape-out is a common milestone.

Coverage: When Is It Done?

You can't test everything, so how do you know when to stop? Coverage measures what has been exercised:

• Code coverage says which lines of RTL ran, and which signals toggled. It is automatic, but it says nothing about whether the checks were correct.
• Functional coverage is a list, written by engineers from the spec, of situations that must occur: each instruction, each exception, each pair of instruction types in adjacent pipeline stages, each queue full. It records which ones have been seen.

Teams watch bug rates as well. When random tests run for weeks with no new bug, and coverage holes are closed or justified, the design is near tape-out. There is never a proof that it's finished. It is a judgment based on the evidence. The SoC Verification tutorial covers how the same ideas extend to a whole chip.

Verifying Performance

A processor can be functionally correct and still be too slow. Performance bugs don't produce a wrong answer, so ordinary tests never see them. Teams run performance regressions, comparing cycle counts on key programs with the performance model and with earlier RTL versions. A simple rule-based model can act as a checker on a small core: if measured cycles differ from the prediction, something has changed. A sudden gain of a few percent in cycles often means that a stall crept in.

Who Does the Work

Verification engineers often outnumber designers on a CPU project. They write test plans from the spec, build the checkers, run regressions of many thousands of tests each night, and sort the failures. A failure must be classified: is it an RTL bug, a test bug, or a model bug? Each one needs a person to read a waveform and find the first wrong cycle. As a project gets near tape-out, a rising share of the failures are in the tests, and the rate of real bugs falling toward zero is the signal that everyone is watching.

Common Mistakes