Model checking

Notes

Symbolic model checking with BDDs, later augmented by SAT-based methods, made industrial-scale proofs feasible.

Overview

Model checking is an automatic formal verification method that explores the reachable states of a finite-state model of a design to decide whether a property, usually written in temporal logic, holds in every case. When the property holds the tool reports a proof; when it fails the tool produces a counterexample, a concrete sequence of inputs and states that shows how the failure happens. In chip design it is the engine inside formal property verification tools that check assertions on RTL.

How it works

The tool first turns the RTL into a state transition system: the registers hold the state, and the logic between them defines which next states are possible for each input. Properties describe what must always be true, for example that two grants are never given in the same cycle, or what must eventually happen, for example that every request is answered. Assumptions restrict the inputs to legal behaviour, so the tool does not report failures that the real environment could never cause.

Rather than listing states one by one, which would be impossible for real designs, model checkers reason about large sets of states symbolically, and modern engines rely heavily on Boolean satisfiability (SAT) solvers. Bounded model checking asks whether a property can fail within a fixed number of clock cycles from reset, which is good at finding bugs quickly; full proofs must show the property holds at every depth.

The main limit is state explosion: each extra register can double the number of possible states. Proofs on large blocks may fail to converge, and engineers respond with abstraction, partitioning the design, adding constraints, strengthening properties or settling for a bounded result. For that reason teams usually apply model checking to blocks and properties where exhaustive proof is most valuable, such as control logic, arbiters, protocols, coherency and security rules, and keep simulation and emulation for the rest.

Examples

• Proving that an arbiter never grants the bus to two masters in the same cycle, for all possible request patterns.
• A counterexample trace, shown as a waveform, revealing a deadlock in a cache coherency protocol that needed a rare sequence of messages.
• Bounded checks run on a new RTL block before its simulation testbench is ready.
• Early academic use on industrial bus protocols, with Carnegie Mellon researchers applying symbolic model checking to the Futurebus+ and PCI local bus protocols.

Why it matters

Related terms

• BMC
• Counterexample
• State space explosion
• Formal verification

Where it appears on the Hub

Used on 7 pages of the Hub. In each group, the pages that mention it most come first.