formal verification
Imagine you've built a digital lock, and you want to be sure it can never open without the right code. With simulation, you'd type in a few thousand wrong codes, watch it stay shut each time, and feel pretty good — but you've only checked the codes you happened to try. Formal verification takes the opposite approach: instead of testing examples, it proves — using mathematics — that no possible input, in any order, can ever pop the lock open. One airtight proof stands in for an infinity of trials.
Concretely, a formal tool takes your design (the RTL) plus a property you write — a precise statement like "the grant signal is never asserted to two masters at once" — and reasons over the entire reachable state space of the circuit as a mathematical structure. If the property holds under every legal input sequence, the tool returns proven. If it doesn't, the tool hands you a concrete counterexample: an exact waveform showing the steps that break it. There's no "did we write enough tests?" anxiety, because the search is exhaustive by construction. This makes it the natural partner to assertions — the constructs you use to state those properties, typically in SystemVerilog Assertions (SVA).
The catch is in the word exhaustive. It applies only to the property you stated and the design block you pointed it at — formal proves that claim completely, not that your chip is correct overall. And the reachable state space grows explosively, so large blocks can blow past memory or time limits, forcing you to constrain inputs, decompose the problem, or accept a bounded proof that holds only out to N clock cycles. Formal is razor-sharp on control logic, arbiters, and protocol checks; it's the wrong tool for verifying a wide datapath multiplier, where constrained-random simulation still earns its keep.
// At every clock edge (outside reset), at most one grant is asserted.
property p_grant_mutex;
@(posedge clk) disable iff (rst)
$onehot0(grant);
endproperty
a_grant_mutex: assert property (p_grant_mutex);The "two masters" property above, written as a vendor-neutral SystemVerilog concurrent assertion, says that grant is one-hot at most — at most one bit set on any clock. A formal tool either returns proven — no reachable state ever drives two grants high — or a counterexample waveform showing exactly how two masters get granted at once.
"Formal verification" and "model checking" are often used interchangeably, but model checking is really one technique under the formal umbrella (alongside equivalence checking and theorem proving). The shared idea is a guarantee that comes from mathematical proof over all cases, not from running examples.