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.

For more information please contact Ofer Shtrichman