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 P_{i} . Focusing on potential bugs in a specific cycle can be formulated by simply restricting the disjunction over P_{i} 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 ModelChecker), 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 
IBM CPU Part #1 
18 
9685 
55870 

2 
IBM CPU Part #2 
5 
3628 
14468 

3 
IBM BIU 1996 
14 
14930 
72106 

4 
IBM PowerPC BIU #1 
24 
28161 
139716 

5 
IBM Arbiter #1 
12 
9396 
41207 

6 
IBM LSU 1997 
22 
51654 
368367 

7 
IBM Arbiter #2 
9 
8710 
39774 

8 
Galileo FIFO #1 
35 
58074 
294821 

9 
Galileo FIFO #2 
38 
63624 
326999 

10 
IBM PowerPC BIU #2 
31 
61088 
334861 

11 
IBM Cache Control #1 
32 
32109 
150027 

12 
IBM PowerPC BIU #3 
31 
39598 
19477 

13 
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 BDDbased 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