Bounded Model Checking

1 P02c00 bmc 2008/11/20 10:13 page 457 #3 Handbook of SatisfiabilityArmin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.)IOS Press, 2009c 2009 Armin Biere and IOS Press. All rights 14 Bounded Model CheckingArmin BiereBesides Equivalence Checking [KK97, KPKG02] the most important indus-trial application of SAT is currently Bounded Model Checking (BMC) [BCCZ99].Both techniques are used forformalhardware verification in the context of elec-tronic design automation (EDA), but have successfully been applied to manyother domains as well. In this chapter, we focus on practice, BMC is mainly used for falsification resp. testing, which is con-cerned with violations of temporal properties.

2 However, the original paper onBMC [BCCZ99] already discussed extensions that can prove properties. A con-siderable part of this chapter discusses these complete extensions, which are oftencalled unbounded Model Checking techniques, even though they are build uponthe same principles as plain further related applications , in which BMC becomes more and moreimportant, are automatic test case generation for closing coverage holes, anddisproving redundancy in designs. Most of the techniques discussed in this chaptertransfer to this more general setting as well, even though our focus is on propertyverification resp. basic idea of BMC is to represent a counterexample-trace of boundedlength symbolically and check the resulting propositional formula with a SATsolver.

3 If the formula is satisfiable and thus the path feasible, a satisfying assign-ment returned by the SAT solver can be translated into a concrete counterexampletrace that shows that the property is violated. Otherwise, the bound is increasedand the process repeated. Complete extensions to BMC allow to stop this processat one point, with the conclusion that the property cannot be violated, hopefullybefore the available resources are Model CheckingThe origins of Model Checking go back to the seminal papers [CE82] and [QS82].Clarke, Emerson and Sifakis won the 2007 Turing Award for their pioneeringwork on Model Checking . A workshop affiliated to the Federated Conference onLogic in Computer Science (FLOC 06) celebrated the 25th anniversary of modelchecking.

4 The proceedings [VG08] of this workshop andthemodel Checking p02c00 bmc 2008/11/20 10:13 page 458 #4 458 Chapter 14. Bounded Model Checking [CGP99] are good starting points to learn about Model Checking . A more recentsurvey [PBG05] adds a perspective on SAT-based Model this chapter, we focus on SAT-based symbolic Model Checking [McM93],which originally relied on binary decision diagrams (BDDs) [Bry86] to symbol-ically represent systems. Operations on system states can then be mapped toBDD operations. In practice, BDDs can handle circuits with hundreds of latches,but often blow up in [BCCZ99] was an attempt to replace BDDs with SAT in symbolic modelchecking.

5 However, SAT lacks the possibility to eliminate variables, which is akey operation in BDD-based Model Checking . The solution in BMC is to focuson falsification and, at least in a first approximation, drop completeness. Thisparadigm shift was hard to convey originally, but was accepted at the end, sinceSAT-based Model Checking , at least for falsification, scales much better [Kur08].Another important direction in Model Checking is explicit state Model check -ing. The SPIN Model checker [Hol04] is the most prominent explicit state modelchecker and is mainly used for Checking protocols. It draws its main power frompartial order reduction techniques such as [Pel94]. Related techniques exist inBMC as well, see for instance [Hel01, JHN03].

6 However, for the rest of this chap-ter we focus on symbolic techniques for synchronous systems, for which partialorder techniques do not seem to first decade1of research in Model Checking witnessed a heated debateon which specification formalism is more appropriate: linear time logic versusbranching time logic. Commonly only computation tree logic (CTL) [CE82], abranching time logic, and linear time logic (LTL) [Pnu77] are used. Originally,LTL was called propositional temporal logic (PTL) as a special case of full first-order temporal logic. However, nowadays LTL without further qualificationis solely used for propositional linear temporal logic. Also note that PTL is also anacronym for past time (propositional) linear temporal, see for instance [BHJ+06].

7 LTL is arguably easier to understand and use, but at least in theory, LTLis harder [SC85] to check than CTL. If the system is represented symbolically,there is actually no difference as both problems are PSPACE complete [SC85,Sav70, PBG05]. Specifications in practice are typically in the intersection [Mai00]between LTL and CTL. If we restrict ourself to properties in the intersection, theproblem of choosing between LTL and CTL boils down to which Model checkingalgorithm to use. In this respect, BDD-based Model Checking has a slight biastowards CTL, whereas SAT-based Model Checking has a bias towards LTL. Thus,we mainly focus on LTL in the rest of this chapter. Further details on temporallogic and its history can be found in [Eme90, Var08].

8 LTLAs first promoted by Pnueli [Pnu77], temporal logic is an adequate specificationformalism for concurrent resp. reactive systems. The syntax of the linear temporallogic LTL contains propositional boolean variablesV, temporal operators and theusual propositional operators, including negation and conjunction . Typical1A similar discussion took place in the recent process of standardizing temporal logic in theform of System Verilog Assertions (SVA) and the Property Specification Logic (PSL). p02c00 bmc 2008/11/20 10:13 page 459 #5 Chapter 14. Bounded Model Checking459temporal operators are the next time operatorX, the finally operatorF,andthe globally of temporal formulas are as follows:a Xbmeans the propertybhas to hold in the next time instance, unlessadoes not hold now.

9 WithXaloneonly properties about a finite future around the initial state can be other temporal operators allow to extend this finite view, and specify infinitebehavior. The globally operatorGallows to specifysafety propertiesin formof invariants or assertions that need to hold in all reachable states. For instance,G (a b) specifies mutual exclusion weconsider, the finally operator, describes necessary behavior, (a Fb),which requires eachato to be followed byb. More verbosely, the followinginvariant holds: ifais true then at the same time or laterbhas to hold, be postponed forever, afterahas been assured. This is an invariant witha (potentially) liveness condition interpretation of propositional variables may change over time but isuniquely determined by the current state of the Model .

10 This correspondence iscaptured via a labelling functionL:S IP (V), whereSis the set of states. Apropositional variablepis true in a system statesiffp L(s). Beside the setof statesS, a Model has a setI Sof initial states, and a transition relationT S S. Such a Model is also calledKripke structure. Often only modelsisomorphic to the set of interpretations of the boolean variablesVare considered:thenS=IP(V)andL(V )=V for all states s=V V. A typical exampleare models of synchronous circuits, whereVis the set of latches and input signals,and optionally includes output and internal signals as well. In the following, wefix one Kripke structureK=(S, I, T, L) transition relationTis assumed to be total and the setIof initial statesto be nonempty.