7
\$\begingroup\$

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?

\$\endgroup\$
4
  • 8
    \$\begingroup\$ whoever voted to close this as "about the use of electronic devices, not their design": you're very, very far off. This is a core electrical (digital) engineering question, with a solid history of scientific literature in this field, which ferris even cites; it doesn't get much further from using existing devices than this question! \$\endgroup\$ Nov 13, 2021 at 12:03
  • \$\begingroup\$ @Null: re your last edit (changing the formatting of "path" in the first property description) - is this correct? I left that out originally in order to match the formatting of the referenced paper. \$\endgroup\$
    – ferris
    Nov 15, 2021 at 13:49
  • \$\begingroup\$ @ferris It is the English word "path", not the multiplication of variables "p", "a", "t", and "h" so, yes, the proper formatting would be using \mathrm whether or not the original paper used it. You are not quoting the paper so I think it makes sense to format it properly. \$\endgroup\$
    – Null
    Nov 15, 2021 at 13:55
  • \$\begingroup\$ @Null thanks for the clarification, agreed! \$\endgroup\$
    – ferris
    Nov 15, 2021 at 14:03

1 Answer 1

3
\$\begingroup\$

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.

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.