Unbounded Model Checking

Part of the Series on Integrated Circuits and Systems book series (ICIR)

SAT-based Bounded Model Checking (BMC) [45, 66, 109, 178] has been shown to be more robust and scalable compared to symbolic model checking methods based on Binary Decision Diagrams (BDDs) [12, 17]. Unlike BDD-based methods, BMC focuses on finding bugs of bounded length, successively increasing the bound to search for longer traces. Although BMC can find bugs in larger designs than BDD-based methods, the correctness of a property is guaranteed only for the analysis bound. A completeness bound has been proposed [66, 67, 72], to provide a proof of correctness for safety properties based on the longest loop-free path between states. Unfortunately, the longest loop-free path can be exponentially longer than the reachable diameter of the state space (for example the longest loopfree path for an n-bit counter is 2n while the reachable diameter is 1). One can use inductive invariants like reachability constraints [73] to obtain proofs earlier than the longest loop-free path. Alternatively, one can obtain a shorter completeness bound, i.e., the longest shortest backward diameter, for BMC using SAT-based fixed-point computations [67], described in the procedure Fixed_point_EF (see Figure 2.10). Such an approach uses cubewise enumeration of SAT solutions, as described in the procedure All_sat (see Figure 2.9), for computing exisitential quantifications.


Model Check Conjunctive Normal Form Satisfying Assignment Liveness Property Bounded Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media, LLC 2007

Personalised recommendations