k-induction
Beginner
A proof that works like falling dominoes. If a rule holds for a run of steps, it must hold for the next step too.
Novice
A two-part proof, like showing that a row of dominoes will all fall: first show the rule holds for the first cycles, then show that any good cycles in a row are always followed by another good one.
Expert
The second part starts from any state at all, including states the design can never reach, so it can fail on a harmless state. Remedies: a larger , requiring the states on the path to differ, or helper assertions. SymbiYosys’s smtbmc engine uses it in prove mode.
Explained in Verification (Design Flow).
See also: Bounded model checking (BMC), IC3 / PDR.