A proof task arrives as one line in a plan, and somebody must choose how to attack it: bounded search for the quick bug, induction for the control invariant, a learning engine when no helper is in sight, abstraction when the state space dwarfs every engine. The wrong choice costs days. This lesson is the menu those choices are read from.
Every engine below answers the same reachability question and differs in what it can conclude. Only an exact or inductive argument proves; only a search from reset refutes. Exact BDD reachability computes the reachable set itself, so it proves and refutes, at a cost set by diagram size. Bounded search unrolls a fixed number of steps: it refutes with a counterexample or reports bounded to N, and never proves unbounded safety alone. K-induction checks a base case from reset plus a step from arbitrary states: a pass proves, and only the base case refutes, because a step failure may start from an unreachable state and is inconclusive on its own. Interpolation and IC3-style learners build their own over-approximations and invariants: they can prove without a hand-written helper but can stall on wide datapaths. Abstraction refinement shrinks the model, proves or refutes on the small one, and refines when the counterexample is spurious.
Tools run these as a portfolio, trying several in parallel and keeping whichever answers first. That is why the same property can be proven by induction on one design and by a learning engine on the next: which engine finishes first is a property of the design, not of the property shape.
Engine | Can prove | Can refute | Cost driver | Common failure |
|---|---|---|---|---|
BDD reachability | Yes, exact fixed point | Yes, a shortest trace from the layers | Diagram size under the variable order | Order blow-up on arithmetic and wide state |
Bounded search | No: bounded to N only | Yes, shortest trace | Gates times depth | A bug past the bound is invisible |
K-induction | Yes, base and step to the same k | Only through its base case; a step failure alone is inconclusive | Window k, helper quality | Non-inductive property, CTI from an unreachable state |
Interpolation | Yes, when the over-approximation closes | Yes, when the bounded check from the real reset finds a trace; from an approximated start a failure only lengthens the bound | Proof width, datapath | Does not converge on arithmetic |
IC3 or PDR | Yes, via a grown inductive invariant | Yes, a concrete trace once a blocked state reaches reset | Clause learning, state bits | Stalls on deep counters and wide data |
Abstraction refinement | Yes, on the small model, if it over-approximates | Yes, once the trace replays on the full model | Refinement rounds | Spurious traces never end |
The plan names an engine per property family, not one engine for everything.
Every bounded entry carries its depth and its justification, never a bare pass.
Properties that need induction name their helpers, and every helper is itself proven.
Match the design to the engine before the run, with the ladder above: control-dominated logic with clean invariants favours induction; wide arithmetic favours bounded search plus abstraction; deep counters favour induction or a counter abstraction, because a bound would have to reach the depth; unknown territory favours the portfolio with a time budget. When the run disagrees with the choice, the convergence topic tells you which measurement to take first.
No. The bounded pass says nothing beyond its depth, and the inconclusive run says nothing at all. The property is unproven until induction, or another unbounded engine, passes on the same model and assumptions.