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 |
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 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, 1999The 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