Model checking
Beginner
A proof that looks at every situation a design can ever get into, to see if a rule can be broken.
Novice
A formal method that treats the design as a machine moving from state to state, one step per clock cycle, and checks whether any state it can reach breaks a rule.
Expert
Symbolic engines (BDD reachability, SAT-based bounded model checking, k-induction, interpolation, IC3/PDR) represent huge sets of states as formulas instead of listing them one by one. Production tools run several engines at once and take whichever answers first.
Explained in Verification (Design Flow).
See also: Bounded model checking (BMC), k-induction, IC3 / PDR.