Formal verification
Beginner
Using math to prove a design follows a rule for every possible input, without running tests one by one.
Novice
Checking a design by mathematical proof instead of by running tests. A tool considers every possible input at once and either proves that a rule always holds or produces a counterexample: one specific input sequence that breaks it.
Expert
Exhaustive within its assumptions and any depth limit. The number of possible states doubles with every storage bit added (state explosion), so it is applied block by block, with assumptions about inputs and simplifications of the design.
Explained in Verification (Design Flow).
See also: Model checking, Logical equivalence checking (LEC), Counterexample (trace).