Formal Verification Introduction

Everything in Sections A and B — directed tests, constrained-random stimulus, coverage — shares one structural limit: each is a sample. However many transactions a regression runs, it's still a finite number of specific traces through a design's behavior, never all of them. Formal verification is a categorically different technique: instead of sampling, it treats the RTL and a property together as a mathematical problem, and either proves the property holds in every reachable state or proves it doesn't, with the exact sequence of inputs that breaks it.

What "exhaustive" actually means here

A formal tool doesn't run the design forward with specific input values the way a simulator does. It explores the design's entire reachable state space — every state combination the sequential logic could possibly reach from reset, considering every possible input at every step — and checks the property against all of it at once. A property simulation never happened to violate might still be provably false, if some legal-but-unexercised sequence of inputs would break it. Conversely, a property formal proves true is true for every input sequence that could ever occur, not just the ones anyone thought to write a test for.

The real limit: state explosion

This exhaustiveness has a genuine, structural cost. The number of reachable states grows roughly exponentially with the number of state-holding elements (flip-flops, latches) in the logic being analyzed — a property that's trivial to prove over a handful of registers can become computationally intractable over a few hundred. This is why formal verification is applied at the block or unit level, against carefully chosen properties, not run exhaustively across an entire full-chip design — the state space of a modern SoC is far beyond what full exploration can practically cover.

Two different engineering answers exist to this limit, with a real, honest tradeoff between them:

• Bounded model checking (BMC) — unroll the design's behavior for a fixed number of cycles (say, 50) and exhaustively check every possible trace within that bound. Fast and scalable, but incomplete by construction: a bug that only appears after cycle 51 is invisible to a 50-cycle bound, and "no bug found within the bound" is not the same claim as "no bug exists."
• Unbounded proof techniques (full state-space exploration, or techniques like k-induction that extend a bounded proof into a true for-all-time guarantee) — give the actual "proven for every possible trace, of any length" result BMC can't, at the cost of being harder to converge and more sensitive to the design's actual size.

How k-induction actually gets from "bounded" to "for all time": it adds a second step on top of an ordinary BMC run. The base case is exactly BMC — check the property holds for the first k cycles from reset. The inductive step asks a different question entirely: assuming the property already holds for any k consecutive cycles (not necessarily starting from reset — an arbitrary window), does it still hold on cycle k+1? If both the base case and the inductive step check out, the property is proven for every reachable cycle, not just the first k — the same logical structure as mathematical induction, applied to hardware states instead of numbers.

Why formal complements simulation rather than replacing it

Neither technique's weakness is the other's: simulation can run a design of essentially any size, but can never give an exhaustive guarantee for even one property, only ever more samples. Formal gives a genuine exhaustive guarantee, but only practically reaches block/unit-sized pieces of logic and specific, chosen properties. A real verification effort uses both — formal on the specific control logic, arbiters, and protocol corners where an exhaustive guarantee is worth the setup cost and reachable in practice; simulation-based CDV (Sections A–B) everywhere else, and at full-system scale formal fundamentally can't reach.

Simulation: samples individual traces through the state space
  ●───────►
   ●──────────►
      ●────►
         (some traces run; most of the space untouched)

Formal: proves a property across the entire reachable state space at once
  ┌─────────────────────────────┐
  │ ░░░░░░░░░░░░░░░░░░░░░░░░░░░░ │  ← every reachable state considered
  └─────────────────────────────┘

What's next

The next page covers the two major, distinct ways formal is actually applied in practice — proving properties (an exhaustive version of the assertions SystemVerilog already covers) and equivalence checking (proving two different representations of the same design compute the same thing).