Bounded Model Checking

In Bounded Model Checking (BMC) [BCCZ99], a rather newly introduced problem in formal methods, the task is to check whether a given model M (typically a hardware design) satisfies a temporal property P in all paths with length less or equal to some bound k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and in fact if the property is in the form of an invariant (Invariants are the most common type of properties, and many other temporal properties can be reduced to their form. It has the form of 'it is always true that ... '.), it has a structure which is similar to many AI planning problems.

The general structure of BMC invariant formulas is the following:

Where:

is the initial state,

is a formula representing the transition between cycles i and i+1, and

is the property in cycle i.

It is not hard to see that this formula can be satisfied if and only if there exists a reachable state in cycle i (i £ k) which contradicts the property Pi . Focusing on potential bugs in a specific cycle can be formulated by simply restricting the disjunction over Pi to the appropriate cycle.

Normally verification with BMC is based on a gradual process, where k is increased until either a bug is found or the problem becomes intractable. There is also an upper bound D, called the diameter of M, beyond which there is no point to look for bugs, i.e. it can be proven that if the SAT instance corresponding to k = D is unsatisfiable, then M satisfies P for every path length. In mathematical logic terms, this means that for a large enough k, this method is complete.

A tool called (BMC), originally developed by Armin Biere, takes an SMV - compatible model (SMV is a popular description language in model checking) and a bound k, and generates a propositional SAT instance according to the above equation. The size of the generated formula is linear in k, and indeed empirical results show that k strongly affects the performance. As a second step, BMC transforms the formula to CNF.

The Benchmark instances

The 13 SAT instances given in the benchmark set are all taken from real industrial hardware designs, a contribution of the verification technologies department in the IBM research Laboratory in Haifa (home of RuleBase, the IBM Corporate Model-Checker), and Galileo (a leader in communication hardware design and a heavy user of model checking). In all cases the property is in the form of an invariant.

All the instances are satisfiable. The fourth column, titled 'k', indicates the number of cycles which the transition was 'unrolled' (e.g. k = 10 means that the bug can be found after 10 cycles. This is similar to the 'number of steps' indication in planning problems). The fourth and fifth columns indicate the number of variables and clauses, respectively.

 # Instance Description k #vars #clauses 1 bmc-ibm-1.cnf IBM CPU Part #1 18 9685 55870 2 bmc-ibm-2.cnf IBM CPU Part #2 5 3628 14468 3 bmc-ibm-3.cnf IBM BIU 1996 14 14930 72106 4 bmc-ibm-4.cnf IBM PowerPC BIU #1 24 28161 139716 5 bmc-ibm-5.cnf IBM Arbiter #1 12 9396 41207 6 bmc-ibm-6.cnf IBM LSU 1997 22 51654 368367 7 bmc-ibm-7.cnf IBM Arbiter #2 9 8710 39774 8 bmc-galileo-8.cnf Galileo FIFO #1 35 58074 294821 9 bmc-galileo-9.cnf Galileo FIFO #2 38 63624 326999 10 bmc-ibm-10.cnf IBM PowerPC BIU #2 31 61088 334861 11 bmc-ibm-11.cnf IBM Cache Control #1 32 32109 150027 12 bmc-ibm-12.cnf IBM PowerPC BIU #3 31 39598 19477 13 bmc-ibm-13.cnf IBM Cache Control #2 14 13215 6572

The first 10 instances could be solved with the methods described in [S00], while the 3 last ones could not be solved (they are known to be satisfiable because we used standard BDD-based model checkers to verify them). The accurate results achieved with these designs under various heuristics are listed in the above reference. The SAT solver Chaff is able to solve all 13 designs in about 8 minutes on a Pentium III. / 700 Mhz.

Bibliography

Bounded model checking was introduced in:

[BCCZ99] A. Biere and A. Cimatti and E. Clarke and Y. Zhu, Symbolic Model Checking without BDDs, In the Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS99), lncs, springer, 1999

The results for the benchmark are given in:

[S00] Ofer Shtrichman, Tuning SAT checkers for Bounded Model Checking, In E.A. Emerson and A.P. Sistla Eds, Proc. of Computer Aided Verification 2000 (CAV2000), lncs, springer.