Why is BMC/k-induction used in RTL formal verification?

Question

One popular approach for proving safety properties in formal verification of RTL designs is a combination of BMC and \$k\$-induction, which appears to stem from "Checking safety properties using induction and a SAT-solver".

This boils down to trying to prove:

$$\forall i.\forall s_0...s_i.(I(s_0) \land \mathrm{path}(s_{[0..i]})\rightarrow P(s_i))$$

In other words, that all paths that start at initial states always lead to states which satisfy property \$P\$.

However, it seems that checking repeated applications of a system's transition relation \$T\$ is not necessary to prove a particular property \$P\$ holds for that system.

It seems intuitively that it would instead be sufficient (and potentially cheaper computationally) to prove the following:

$$\forall s.(I(s)\rightarrow P(s)) \land \forall \langle s_i,s_j\rangle.(T(s_i,s_j) \land P(s_i)\rightarrow P(s_j))$$

In other words, proving that all initial states satisfy property \$P\$ and all applications of \$T\$ on a state that satisfies \$P\$ produces a new state that also satisfies \$P\$.

At least for simple system descriptions, this seems easy to do with a (SAT/SMT/similar) solver.

So, what's wrong with the above intuition? Is it computationally more complex than BMC/\$k\$-induction? Is it too difficult to constrain the set of valid states to be equivalent to the set of reachable states? Does it produce less useful error traces when counterexamples are discovered? Or am I missing something else entirely?

Answer 1

Short answer

Simple induction as suggested works for properties that are themselves inductive. For properties that are not inductive, they may be able to be proved by strengthening, and BMC/\$k\$-induction is one method for doing this that's (relatively) effective, easy to work with, and easy to understand/implement.

Long answer

Inductive properties

The proposed approach in the question, i.e. proving:

$$\forall s.(I(s)\rightarrow P(s)) \land \forall \langle s_i,s_j\rangle.(T(s_i,s_j) \land P(s_i)\rightarrow P(s_j))$$

is sufficient for a particular class of (safety) properties, so-called inductive properties, and is not only equivalent to \$k\$-induction for \$k=1\$, but is also in fact the very definition of such properties!

An example of an inductive property \$P\$ over a system \$S\$ is the following:

$$S\triangleq\{x\in \mathbb{Z}\}$$ $$I\triangleq x=0$$ $$T\triangleq x'=x+1$$ $$P\triangleq x\geqslant 0$$

In contrast, an example of a weaker, non-inductive property \$Q\$ over the same system is the following:

$$Q\triangleq x \neq -1$$

While \$Q\$ holds for the initial state of the system, the inductive step fails with the following counterexample:

$$x=-2\land x'=-1$$

Of course, by inspection, we can clearly see that this counterexample is spurious, because the state where \$x=-2\$ is not reachable from the initial \$x=0\$ state. In other words, we know that \$Q\$ is an invariant over \$S\$, but simple induction is not sufficient in order to prove it.

Property strengthening

If a given property can not be proven with induction, it's sometimes possible to simply replace it with a stronger property (for example, using \$P\$ in the place of \$Q\$ above). Informally, this can be seen as "closing the gap" between the set of (in)valid states and the set of reachable states.

In cases where such simple substitution is infeasible, inconvenient, or both, an attempt can be made to strengthen the property. Somewhat more formally, for a non-inductive property \$P\$, a search is conducted to find some other property \$F\$ such that \$I\rightarrow F\$, \$F\$ is inductive, and \$F\rightarrow P\$.

BMC/\$k\$-induction is a particular algorithm that performs such a search which happens to be relatively effective (especially at finding short counterexamples from initial states). Additionally, it's easy to understand/use (especially for people who are not necessarily familiar with formal logic) and implement on top of existing (incremental) SAT/SMT solvers.

For the curious, I'll refer to again to "Checking safety properties using induction and a SAT-solver" for a description of BMC/\$k\$-induction in the context of RTL formal verification, "The \$k\$-induction Principle" for a more formal description of how \$k\$-induction in particular works, and for a (somewhat arbitrary) alternative approach, "Understanding IC3", which also provides some historical context on these methods and their advantages/disadvantages.