Verification

Two different questions get checked between the first RTL and the finished layout. The first is whether the RTL does what the specification intends. Nothing upstream can answer that automatically, because the specification is mostly prose; that is functional verification, the subject of this chapter. The second is whether each later transformation (synthesis into gates, insertion of test logic, layout) preserved the RTL’s behavior. Equivalence checking answers the second question formally. A 1998 study already named the first as the hardest verification problem for most designs, and simulation as its workhorse.¹

Production flows combine several techniques, each covered below:

• Constrained-random simulation: the computer generates legal random inputs, and checkers compare the design’s behavior with a model of what it should do.
• Assertions and coverage: rules checked on every cycle, and counters that record which planned situations the tests actually reached.
• Formal property verification: mathematical proof that a rule holds for all inputs, on blocks small enough to analyze.
• Emulation and FPGA prototyping: running the design in hardware, fast enough for operating systems and long software tests.
• Gate-level and power-aware simulation: targeted reruns on the synthesized gates, and on the design with its power switching modeled.

Progress is planned, measured and reviewed against written criteria. OpenTitan, an open-source security chip project, publishes its own. A block reaches its V1 stage with a reviewed testplan (the list of features to test and how). V2 requires 90% code and 90% functional coverage, with above 90% of tests passing in nightly runs over many random seeds. V3, the final stage, requires 100% code and functional coverage (with waivers for any items left out) and every seed passing.⁶ Each of its random tests runs with 100 different seeds in the nightly regression.⁵

Code and functional coverage at OpenTitan V2

90%

Coverage at OpenTitan V3, with waivers

100%

Seeds per random test, OpenTitan nightly

100

Cost of the 1994 Pentium FDIV replacement

$475M

The staffing follows from the costs. A bug found in simulation costs an edit and a rerun. A bug found in silicon costs a new mask set and months of schedule, and one that ships can cost a recall, as Intel’s Pentium division bug did.³ So teams accept spending more engineering effort on verification than on writing the design.¹

Two inputs often arrive late and cause trouble. The first is the UPF power intent, which says which regions of the chip can be powered down and which special cells guard them. If it joins the simulations only near the end, bugs in the logic that sequences power-down and power-up surface late and are slow to trace; one Samsung team built checkers generated from the UPF to find them earlier.²⁷ The second is the gate-level netlist and its SDF delays, which exist only after synthesis and layout, so the list of gate-level tests has to be planned before they arrive.

Among the outputs, sign-off reviewers look hardest at the merged coverage database and its exclusions. An exclusion removes a coverage item from the total, so each one needs a reason. OpenTitan sorts them into categories: unreachable code (UNR), simulation-only code that never becomes hardware (NON_RTL), features of reused IP that this chip doesn’t use (UNSUPPORTED), items already covered in another testbench (EXTERNAL), and items too hard to hit and judged low-risk (LOW_RISK). It reviews them.⁵

Testbench architecture

A production testbench is layered, so that each layer can be reused and replaced on its own. From the bottom up:

1. Sequences produce transactions, whole operations such as “burst-write 16 words to this address.”
2. Drivers convert each transaction into pin activity, obeying the interface’s timing protocol cycle by cycle.
3. Monitors sit passively on every interface and turn pin activity back into transactions.
4. A transaction-level reference model predicts the expected result of each input transaction, usually without modeling exact cycle timing.
5. Scoreboards and coverage collectors consume the monitors’ output: the scoreboard compares observed with predicted, and the coverage collector counts which situations occurred.

The checking has to stay independent of how the stimulus was generated, either through the scoreboard or through assertions; otherwise a new test needs new checks.⁵ In UVM, an agent bundles the sequencer, driver and monitor for one interface. The factory is a registry that builds every component, so a test can tell it “build my error-injecting driver wherever the normal driver is requested” without editing the environment.¹⁰ The library follows IEEE 1800.2, and its point is verification IP (ready-made agents for standard interfaces) that works across tools and projects.⁸

Simulators and unknown values

Python-based flows are a serious option. cocotb embeds a Python interpreter in the simulator and runs each test as a coroutine, a function that pauses until a given time or signal change. It reaches Icarus Verilog, Verilator, GHDL, NVC and the commercial simulators through their standard C programming interfaces (VPI, VHPI or FLI).¹²¹³

Simulators differ in how they treat unknown values. Hardware languages have a value X, meaning “could be 0 or 1,” for example in a flip-flop that was never reset. Verilator compiles the design into a multithreaded C++ program and is mostly two-state: an X becomes a constant chosen by its --x-assign option, and storage starts at random values, so rerunning with different settings exposes reset bugs. Its support for assertions and functional coverage is partial.¹⁵¹⁶ Four-state simulators keep X, but standard RTL semantics are “X-optimistic”: an if-statement whose condition is X simply takes the else branch, so an uninitialized value can pass quietly in RTL and fail only at gate level. That is why OpenTitan turns on pessimistic X-propagation, which lets the X spread instead, for all its RTL simulations by default.⁵

Stimulus quality

Constrained-random stimulus is only as good as its distribution. A constraint solver that picks uniformly among all legal input combinations can still starve the control logic. Take an ALU (the arithmetic unit of a processor) with several operations. If one operation allows only a few legal operand values while the others allow millions, a uniform pick over all legal combinations almost never chooses that operation, when the useful target is each operation equally often.²³

Engineers bend the distribution with the test language’s controls: weights that make some values more likely (dist in SystemVerilog), ordering hints that make the solver pick the operation before the operands (solve … before), and randomizing whole scenarios first and details second. Coverage reports tell them where to aim. Automatic coverage-directed test generation has been researched for two decades, but published approaches either suit only narrow classes of designs or need a good deal of expert time to set up.²⁵

Coverage and closure

Code coverage (line, branch, condition, toggle, and state-machine states and transitions) costs nothing to write: the simulator derives it from the code. Functional coverage costs engineering time and is only as good as its model. It is written as covergroups, in which coverpoints sort a signal’s values into bins and crosses count combinations of bins, and as SVA cover properties, which count sequences of events.⁵

Code coverage measures activation, not detection. A line holding a bug counts as covered the moment it executes, even if the wrong value it computes is overwritten before reaching an output or a checker.¹ That is why closing code coverage by writing tests that merely reach lines, without checking anything, is a classic way to look done without being done. Closure means sorting every hole into one of four kinds and acting on it: missing stimulus (write or retune a test), missing checker (add a check), unreachable (prove or argue it, then exclude it), or unused feature (exclude it). Exclusions are recorded in reviewed categories.⁵

Formal in a production flow

Formal property verification proves SVA assertions under assumptions, written with assume, that describe the legal inputs. Each property ends in one of three states: proven for all time, failed with a counterexample, or bounded (no failure up to some number of cycles, but no full proof). Assumptions are the danger. If they are too strong, they rule out the very inputs that would break a property, and it “passes” without proving anything; tools report such properties as vacuous.⁷ So engineers pair each important assertion with cover properties showing that the interesting scenarios can still happen.

SymbiYosys runs bounded checks, full proofs, cover searches and liveness checks (“something good eventually happens”), using k-induction in its smtbmc engine and PDR through the ABC tool; Under the hood explains both.¹⁷ OpenTitan sets formal targets alongside its simulation targets. At V1, every input and output of a block must appear in at least one assertion. At V2, 90% code coverage, 75% cone-of-influence coverage (the share of logic that can affect some checked property) and 90% of properties proven in nightly runs. At V3, 100% of properties proven with reviewed assumptions.⁶ One useful trick is the symbolic variable. Instead of writing one assertion per interrupt line, an engineer declares an index that the tool may choose freely, constrained by two assumptions (it is in range, and it never changes after reset). A single property over that index then covers every line.⁷

Formal apps package recurring problems. Connectivity checking turns a spreadsheet of required chip-level connections into proofs.⁷ Equivalence checking is the other everyday formal job: it proves that a changed design, such as a synthesized netlist or a refactored block, still behaves exactly like the original. Yosys’s EQY is an open-source tool for it.¹⁸

Choose the platform by the total time it takes to reach the cycle where the bug lives: compile time plus run time. Software simulation compiles fast and runs slowly, so it wins for short runs; FPGA-based platforms compile slowly and run fast, so they win for very long ones. Bugs also change character over a project. Early bugs show up within a few cycles, and what matters is fast turnaround and full visibility. Later, subtler bugs may need billions of cycles to appear, and on the fast platforms changing which signals are recorded usually means another long compile.²⁶ Commercial emulators (Cadence Palladium, Siemens Veloce, Synopsys ZeBu) sit between the two extremes; Under the hood compares their architectures. The economics of FPGA prototypes, including rented cloud FPGAs, are in Where FPGAs win.

Moving onto hardware raises a testbench problem. A typical UVM or cocotb testbench is object-oriented software that no synthesis tool can turn into gates, so it can’t run on an FPGA.²⁵ Teams either keep it on a host computer and connect it to the design in the emulator, or rewrite stimulus and checking as synthesizable hardware. Software-driven tests fit hardware platforms well: the chip’s own processor runs C programs that exercise the design, and the testbench mostly watches.⁵

Gate-level and power-aware runs

Gate-level simulation (GLS) is kept for what RTL simulation and static checks miss. Because RTL simulation can be X-optimistic, an uninitialized flip-flop, a missing reset or an if-statement on an unknown condition can pass in RTL and fail at gate level.⁵ Zero-delay GLS also catches cases where synthesis read the code differently from the simulator, and exercises the test modes that later stages add. Runs annotated with SDF delays target what static timing analysis models poorly, such as asynchronous interfaces and reset release; they are not how timing is signed off. Expect noise in the other direction too: at gate level, an X that splits and rejoins through different gates can flag failures real silicon would never have, and each one needs analysis.

Power-aware simulation has to exercise the full power-down and power-up sequence in order: enable isolation, save retention state, switch power off, switch power on, restore retention state, release isolation. Static checkers find a missing isolation cell, but not control logic that enables it a cycle late; that needs simulation. A single unknown value from a powered-off domain can spread to thousands of signals within a few cycles, which makes tracing a failure back to its cause slow. Simulation with UPF also takes significantly longer than plain RTL simulation, so teams aim it at tests that switch power modes.²⁷

Vertical reuse is the economic case for the methodology. A UVM agent can run in active mode, where its driver generates traffic, or passive mode, where only its monitor runs. Agents written for a block run active at block level. At subsystem and chip level they run passive: their monitors, assertions and coverage keep checking that block while its real neighbors drive the traffic, and a whole block-level environment becomes a sub-environment of the larger one.¹⁰

At chip level the stimulus shifts to software. Tests written in C and compiled for the on-chip processor exercise the integration, while the testbench supplies models of external devices and watches the pins.⁵ Connectivity moves to formal, where a spreadsheet of required connections becomes a set of proofs.⁷

Sign-off is a staged checklist reviewed by people. OpenTitan’s simulation stages run as follows.⁶

• V1: testplan written and reviewed; the block instantiated in a testbench with its major interfaces connected; a sanity test passing; sanity and nightly regressions set up.
• V2: every planned test written and passing in nightly multi-seed regressions above 90%; 90% code and functional coverage.
• V2S: every security countermeasure tested.
• V3: 100% coverage with waivers, and no failing seeds.

Teams add trend metrics on top: open bugs by severity, the rates at which bugs are found and closed, failure signatures (failures grouped by their first error message) with no owner, and how many weeks the regression has stayed clean. After silicon, every escaped bug gets a root-cause review that asks which plan item, checker or coverage point should have caught it.

The adder computes $\min(255, a + b)$, except that it wraps when both $a$ and $b$ are 240–255. An assertion checks every result, and a 4 × 4 cross of input ranges (0, 1–127, 128–239, 240–255) gives 16 coverage bins, one of which holds the bug. Uniform random stimulus hits it with probability $(16/256)^2 = 1/256$ per test. Weight toward corners picks a range uniformly for each input, then a value inside it, raising that to 1/16. That is the difference between uniform over legal values and uniform over the cases that matter.²³ The directed 255 + 255 test fails at once, and in this view the sim also shows the covergroup and assertion that express the same check. It is coverage-driven debugging in miniature: the empty bin in the grid tells you where to aim before any failure does. A formal tool would find the same counterexample in one query, because it considers all 65,536 input pairs at once.

Below are a cocotb test, the matching SystemVerilog checker and covergroup, a SymbiYosys setup that proves the property, and a nightly regression summary. All are illustrative. The regression log is modeled on typical dashboards and is not the output of any one tool.

For formal, the same property becomes an immediate assertion in a small wrapper module, and SymbiYosys runs it as three tasks. The bounded task searches a fixed number of cycles for a counterexample, the prove task asks the PDR engine for a proof with no depth limit, and the cover task finds a trace that reaches each cover statement.¹⁷ On the buggy adder, bmc and prove both report a counterexample in the corner. After the fix, prove passes and cover still produces a trace, which shows the proof is not vacuous.

[tasks]
bmc
prove
cover

[options]
bmc: mode bmc
bmc: depth 10
prove: mode prove
cover: mode cover

[engines]
bmc: smtbmc
prove: abc pdr
cover: smtbmc

[script]
read -formal sat_add.sv sat_add_props.sv
prep -top sat_add_props

[files]
sat_add.sv
sat_add_props.sv

• Vacuous formal proofs. An assumption that is too strong, or an assertion whose triggering condition can never occur, proves nothing, yet it reports as passing. Formal tools flag such properties as vacuous, and OpenTitan’s formal checklist requires the assumptions to be specified and reviewed.⁷⁶ Pair assertions with cover properties, and review assumptions as carefully as RTL.
• Bounded results treated as proofs. A bounded pass to depth $k$ says nothing beyond cycle $k$. Record the depth, compare it with how many cycles the design needs to reach its deepest states, and push for full proofs on critical properties; OpenTitan’s final formal stage requires every property proven.⁶
• Coverage without observation. Tests written only to reach uncovered lines raise code coverage without checking anything. A line being run (activation) is not the same as its error being seen at an output (observation).¹
• Exclusion creep. Waivers added under schedule pressure turn real holes into “unreachable.” Require a category, a reason and a reviewer for each.⁵
• Platform divergence. FPGA prototypes change clocks, memories and how the design is split across chips, so a pass there is not a pass on the real RTL, and a failure there may be an artifact of the prototype.
• Late power intent. Power sequences tested only late, at full-chip level, leave the timing of isolation and retention control exposed. Static tools catch missing cells, not wrong sequencing.²⁷
• Spec drift. A spec change that never reaches the testplan and the coverage model leaves the regression green while it tests the old behavior.

Constraint solving for random stimulus

Every call that generates a random transaction (randomize() in SystemVerilog) hides two steps. First, solve a constraint-satisfaction problem: find values for the random fields that satisfy every rule. Second, sample: choose one solution among the many that exist, ideally without bias. Two families of solver dominate.

A BDD (binary decision diagram) represents the set of all solutions at once, as a graph of yes/no decisions on each bit with two end nodes, “legal” and “illegal.” Weight each node by how many legal solutions lie below it, walk from the root choosing branches in proportion to those weights, and you land on every legal solution with equal probability, even when some fields are fixed in advance. The cost is size: a BDD for multiplication grows exponentially with the number of input bits whatever order the variables are in, and arithmetic is common in constraints.²³

A SAT or SMT solver (SAT extended with arithmetic on fixed-width numbers) handles arithmetic far better, but it returns one solution per call, and which one depends on its search heuristics, so the results cluster. Generators spread them out by adding blocking constraints that forbid solutions already seen, or by combining the solver with random-walk samplers.²³ A further family adds random hash constraints (XOR formulas over the variables) that slice the solution space into small, roughly equal cells, then picks a cell and a solution inside it. Hashing-based samplers have produced near-uniform stimuli from constraints with more than 100,000 variables. UniGen2 keeps the theoretical guarantees, runs about 20 times faster than the previous state of the art on one core, and speeds up almost linearly with more cores.²⁴

Uniformity is not the real goal, though. Uniform over solutions starves control decisions that have few solutions behind them, such as a rare operation or the top range of an operand.²³ Weighted distributions, solve-before ordering and scenario layers bend the distribution toward the coverage model, which is exactly what the simulation’s corner weighting does.

Coverage metrics, and what they can’t tell you

Manufacturing test has a simple model of what goes wrong (a wire stuck at 0 or at 1), so it can measure what fraction of possible faults a test set detects. Design errors have no such good model, so nobody can prove that a coverage metric tracks the bugs that remain. Every metric is a stand-in, and a way to decide when to stop.²

Code metrics came from software testing and measure controllability: was the statement activated? A bug is detected only if its effect also travels to an output that something checks. OCCOM added that observability. Conceptually, it places a tag on the value assigned in each statement to stand for “this value might be wrong,” then asks whether the tag reaches an output. The share of tags that do is the coverage. Instead of simulating the tags directly, it runs a normal simulation of a slightly rewritten design and then traces tags through a flow graph of the code, which is far cheaper than earlier tag simulators. The result judges a test set more accurately than line coverage.¹

Structural metrics also make automated test generation possible. RFUZZ defines mux-control coverage: every two-input multiplexer (a switch that passes one of two signals) counts as covered when its select signal takes both values within one test. Small extra circuits collect this on an FPGA, and coverage-guided mutational fuzzing, borrowed from software security testing, mutates inputs that reached new coverage to find more.²⁵ Functional coverage remains the engineer’s statement of intent, and code coverage is a check that the intent missed nothing structural. Neither replaces the other.

Model checking: from BDDs to SAT

For a formal tool, a design is a transition system. Write $x$ for the values of all its flip-flops (its state) and $i$ for its inputs in one cycle. Then $I(x)$ is a formula that is true for the initial states (after reset), $T(x, i, x')$ is true when the design can move from state $x$ to state $x'$ under input $i$ in one clock cycle, and $P(x)$ is the safety property, true in every good state. Model checking asks whether any state where $P$ is false can be reached from $I$.

Symbolic model checking with BDDs computes the set of reachable states directly. Start with the initial set, add every state reachable in one more step, and repeat until the set stops growing. It can handle more than $10^{20}$ states, but its BDDs become too large beyond a few hundred state variables, and the result depends on a variable order that is costly to find and for many designs doesn’t exist in a compact form.¹⁹

Bounded model checking replaces BDDs with SAT. It copies $T$ once per cycle, $k$ times, and asks whether $I(x_0) \land T(x_0, x_1) \land \dots \land T(x_{k-1}, x_k) \land \lnot P(x_k)$ can be satisfied: is there a start state, and a sequence of inputs, that leads to a bad state at step $k$? A satisfying assignment is a counterexample. Trying $k = 0, 1, 2, \dots$ in turn yields the shortest one. BMC finds bugs fast thanks to the depth-first way SAT solvers search, uses much less memory than BDDs, and needs no variable order.¹⁹ Its weakness is completeness: “no violation up to $k$” says nothing about step $k + 1$.

k-induction closes the gap in two parts. The base case is BMC to depth $k$. The step case asks whether any path of $k + 1$ states, where $P$ holds in the first $k$, can violate $P$ in the last. Crucially, the path may start from any state at all, not only from reset. If no such path exists, $P$ holds forever. Because the step ignores reachability, it can fail on a path that starts in a state the design never reaches. Requiring all states on the path to differ (loop-free paths) makes the method complete for finite designs, though $k$ may then need to grow as long as the longest such path.²⁰ SymbiYosys’s smtbmc engine runs k-induction in prove mode, with a default depth of 20.¹⁷ In practice, engineers add helper assertions that rule out the unreachable states, so a small $k$ is enough.

IC3 avoids unrolling altogether. It maintains a series of frames $F_0 = I, F_1, \dots, F_k$. Each $F_i$ is a formula true in at least every state reachable within $i$ steps (an over-approximation), each frame contains the one before it, and $P$ holds in all of them. Step by step:

1. Ask SAT whether some state $s$ in the last frame $F_k$ can step into a state that violates $P$.
2. If so, try to block $s$: find the largest frame $F_i$ from which $s$ can’t be reached in one step, shrink “not $s$” to a small clause that still holds, and add that clause to frames $F_1$ to $F_{i+1}$.
3. If $s$ can be reached from the previous frame, its predecessor must be blocked first, so recurse. If a chain of predecessors leads back to the initial states, that chain is a real counterexample.
4. When no bad state remains in $F_k$, add a new empty frame and push each clause forward to later frames wherever it still holds.
5. If two neighboring frames end up with the same clauses, that frame is an inductive invariant: a fact that holds initially, is preserved by every step, and implies $P$. $P$ is proven.

A typical run makes many tens of thousands of cheap, incremental SAT queries, and IC3 placed third in the 2010 hardware model checking competition.²¹ Een, Mishchenko and Brayton named the method property directed reachability (PDR). They found it stronger than interpolation, the previous leading method, on industrial problems, and able to find deep counterexamples, though BMC finds counterexamples better on average.²²

Production formal tools therefore run portfolios: BMC to find bugs, k-induction and PDR for proofs, and simplifications in front, such as cutting away all logic that can’t influence the property (cone-of-influence reduction). SymbiYosys exposes the same idea through its list of engines: smtbmc, abc pdr, and AIGER back-ends for other model checkers.¹⁷

Emulation architectures

The first purpose-built engines, IBM’s Yorktown Simulation Engine and Engineering Verification Engine, were arrays of simple 4-bit processors joined by a crossbar switch. Processor-based commercial emulators descend from them. They break the gate-level design into instructions and schedule those across many simple processors, so compiling is quick and every signal can be recorded without recompiling, at up to a few MHz. The price is very expensive hardware, in the millions of dollars.²⁶

FPGA-based emulators and prototypes instead map the design onto commercial FPGAs. Splitting the design across many devices, then running synthesis and place-and-route for each, makes compiles slow, and observing different signals usually means re-synthesizing. In return, run speed is high and the hardware is cheaper.²⁶ Research platforms explore the space between. Cyclist maps RTL operators (adders, multiplexers, registers) rather than individual gates onto a mesh of small RISC-like processors, aiming for near-FPGA speed with software-like compile times and full visibility.²⁶ Every hardware platform shares one limit: the design and anything mapped with it must be synthesizable, so stimulus and checking either become synthesizable hardware or stay on a host computer.²⁵