Formal verification

Notes

Practical on control logic, arbiters, FIFOs and protocol bridges; datapath and large sequential depth remain difficult.

Overview

Formal verification uses mathematical methods to prove that a design satisfies stated properties for every possible input, rather than for the particular inputs a simulation happens to apply. It either proves a property holds or produces a counterexample showing how it fails, which makes it powerful for finding rare corner-case bugs and for proving that critical behaviour is correct.

How it works

Engineers express the intended behaviour as properties, usually SystemVerilog assertions, together with assumptions that restrict inputs to legal behaviour. A formal tool then explores the design's state space using algorithms such as model checking with SAT and BDD engines. If it finds a sequence of inputs that violates a property, it returns that sequence as a waveform for debugging. If it exhausts all possibilities, the property is proven; if the design is too large, it may give a bounded result, proven for a certain number of clock cycles.

Formal works best on control logic: arbiters, protocol handlers, cache coherence, interrupt controllers and safety mechanisms. Large datapaths and whole chips are usually too big for full proofs, so teams target blocks or use abstraction.

Many formal applications, often called apps, package the method for specific jobs without hand-written properties. Equivalence checking proves that a gate-level netlist matches its RTL, and is routine after synthesis and changes. Others check connectivity, register access, X propagation, clock domain crossings and power intent.

Examples

• Proving that an arbiter never grants two requesters at the same time.
• Finding a deadlock in a cache coherence protocol that simulation had missed for months.
• Running equivalence checking after synthesis to confirm the netlist matches the RTL.
• Using a connectivity app to confirm that every pin of a large SoC is wired to the right block.

Why it matters

Some bugs are almost impossible to hit with simulation, and formal can find them or prove their absence. Formal verification engineers, design verification engineers and RTL designers use it, and safety and security teams value exhaustive proofs. Equivalence checking is part of every digital flow.

In the chip lifecycle formal is used from early RTL, when designers can check blocks before a testbench exists, through verification signoff, and for equivalence checks after every netlist change.

Related terms

• Model checking
• Equivalence checking
• Formal app
• Assumption

Where it appears on the Hub

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