Bounded Model Checking

Bounded Model Checking: 

Bounded Model Checking Presented by Wenkai Tan Nov 5, 2002

Why we need Model Checking?: 

Why we need Model Checking? The obstacle to “help computers help us more” – Design Validation Simulation and testing Formal verification 1. Deductive verification 2. Model checking

What is Model Checking?: 

What is Model Checking? Exhaustively traverses all the reachable states of the system to verify the desired properties + Fully automatic + Gives a counterexample when the desired property is not satisfied - Can only check finite state system - State explosion

The history of Model Checking: 

The history of Model Checking Explicit representation Model Checking -- very small state space, ~220 BDD based Symbolic Model Checking -- 10120, but still not enough Bounded Model Checking with satisfiability solving -- very efficient in safety and liveness properties so far

Explicit representation Model Checking: 

Explicit representation Model Checking Use a Kripke structure M = (S, S0, R, L) to represent the system and temporal logic to describe the desired properties Temporal logic AGp AFP

BDDs and Symbolic Model Checking: 

BDDs and Symbolic Model Checking 1. BDDs are directed, acyclic graphs that hold a compressed form of truth table of a Boolean function 2. BDDs share sub-terms of the function to obtain the compression 3. BDDs are very sensitive to orderings of variables and finding a good ordering is NP-Complete

An example for OBDD: 

An example for OBDD Binary decision tree for the two-bit comparator, f (a1,a2,b1,b2) = (a1↔b1) ∧ (a2↔b2) a1 0 1 b1 a2 a2 0 1 b2 b2 0 1 b2 b2 0 1 0 1 1 0 0 1 0 1 0 1 0 1 0 0 0 0 b1 a2 a2 0 1 b2 b2 0 1 b2 b2 0 1 0 1 0 0 0 1 0 1 0 1 0 0 1 0 0 1

An example for OBDD: 

An example for OBDD a1 b1 a2 0 1 0 b2 0 0 1 b1 1 b2 0 0 1 0 1 1 1 a1 a2 a2 0 1 b1 b1 0 1 b1 b1 0 1 b2 b2 1 0 0 1 0 1 1 0 0 1 1 0 0 1

OBDDs and Symbolic Model Checking: 

OBDDs and Symbolic Model Checking 1. The reachable state-space is represented by a OBDD 2. The property is evaluated recursively, by iterative fix point computations on the reachable state-space 3. The size of the OBDD is typically the bottle-neck of Model Checking

Bounded Model Checking: 

Bounded Model Checking In bounded model checking, we construct a Boolean formula that is satisfiable iff the underlying state transition system can realize a finite sequence of state transitions that reaches certain states of interest.

Bounded Model Checking: 

Bounded Model Checking Bounded model checking based on SAT procedures not BDD, hence 1. Smart DFS search of SAT potentially will get faster to a satisfying sequence (counterexample) 2. No exponential space

Propositional formula of bounded model checking: 

Propositional formula of bounded model checking Given: -- a transition system, M, -- a temporal logic formula, f and -- a user supplied bound, k The unrolled transition relation is [[ M ]]k := I (s0)∧

Propositional formula of bounded model checking: 

Propositional formula of bounded model checking Example: Consider the CTL formula, EFp. We wish to check whether it can be verified in two time steps, i.e., k=2 [[ M, f ]]2 := I (s0)∧T (s0, s1)∧T (s1,s2)∧ ( p (s0)∨ p (s1)∨p (s2) )

Example I: 

Example I 2-bit counter

Safety Property: 

Safety Property Is there a state reachable within k cycles, which satisfies (l∧r) to get counter example. I (s0) : ( ¬l0∧¬r0 ) ∧ T (s0, s1) : ((l1↔l0 r0)∧(r1↔ ¬r0)) ∧ T (s1, s2) : ((l2↔l1 r1)∧(r2↔ ¬r1)) ∧ p (s0) : (l0 ∧ r0 ∨ p (s1) : l1 ∧ r1 ∨ p (s2) : l2 ∧ r2 ) p = AG (¬ l ∨ ¬ r). k = 2

Example II: 

Example II

Liveness Property: 

Liveness Property First let inc (s,s’) = (l’↔l r )∧(r’↔¬r). So, T (s,s’) = inc (s,s’)∨(l∧¬r∧l’∧¬r’) We check the satisfiability of EG(¬l∨¬r) to get counter example for p First, s0, s1, s2 must be part of valid path starting from the initial state Second, the sequence of s0, s1, s2 must be part of a loop p = AF (l ∧ r). k = 2

Liveness Property: 

Liveness Property I (s0) : ( ¬l0∧¬r0 ) ∧ T (s0, s1) : ((l1↔l0 r0)∧(r1↔ ¬r0) ∨ l1∧¬r1∧ l0∧¬r0 ) ∧ T (s1, s2) : ((l2↔l1 r1)∧(r2↔ ¬r1) ∨ l2∧¬r2∧ l1∧¬r1) ) ∧ T (s2, s3) : ((l3↔l2 r2)∧(r3↔ ¬r2) ∨ l3∧¬r3∧ l2∧¬r2) ) ∧ s3 = s0 : ( (l3↔l0)∧(r3↔r0) ∨ s3 = s1 : (l3↔l1)∧(r3↔r1) ∨ s3 = s2 : (l3↔l0)∧(r3↔r0) ) ∧ p (s0) : ( ¬l0 ∨ ¬r0 ) ∧ p (s1) : ( ¬l1 ∨ ¬r1 ) ∧ p (s2) : ( ¬l2 ∨ ¬r2 )

BMC: 

BMC At CMU, a model checker called BMC has been implemented, based on bounded model checking. It’s input language is a subset of the SMV language. It takes in a circuit description, a property to be proven, and a user supplied time bound k. It then generates the propositional formula.

Experimental Results: 

Experimental Results 1. We investigate a sequential shift and add multiplier. We specify that when the sequential multiplier is finished, its output is the same as the output of a certain combinational multiplier.

Experimental Results: 

Experimental Results 2. An asynchronous circuit for distributed mutual exclusion. It consists of n cells and n users. We proved the liveness property that a request for using the resource will eventually be acknowledged. We also add the fairness constraint that each asynchronous gate does not delay execution.

Experimental Results: 

Experimental Results 3. Repeated the experiment 2 with a buggy design, by removing several fairness constraints.

Experiments on Industrial Design: 

Experiments on Industrial Design Experiments on subcircuits from a PowerPC microprocessor of Motorola. To check 20 assertions. First turn each assertion into an AGp property. For each of the properties, 1. Check whether p is a tautology. 2. Check whether p is otherwise an invariant. 3. Check whether AGp hold for various time bounds ,k, from 0 to 20.

Experiments on Industrial Design: 

Experiments on Industrial Design 1. For combinational tautology checking we eliminate all initialization statements and run BMC with a bound of k =0. Under these conditions, the specification could hold only if p was true for all assignments to its state variables.

Experiments on Industrial Design: 

Experiments on Industrial Design 2. Invariance checking entails checking whether the formula holds in all initial states and is preserved by the transition relation. So, first run BMC with all initialization assignments with a time bound of k=0. Then remove all initialization assignments and add initial states predicate, run BMC with a time bound of k=1.

Experiments on Industrial Design: 

Experiments on Industrial Design AGp not holding under these conditions could possibly be due to behaviors in unreachable states. For instance, if an unreachable state s, existed which satisfied p but had a successor s’, which did not, then the check will fail. So, this technique can show that p is an invariant, but can’t show that it is not.

Experiments on Industrial Design: 

Experiments on Industrial Design As a comparison, the results of BDD-based model checking are that SMV was given each of the 20 properties separately, but completed only one of these verifications

Verification Methodology: 

Verification Methodology 1. Annotate each design block with Boolean formulae required to hold at all time points. Call these the block’s inner assertions. 2. Annotate each design block with Boolean formulae describing constraints on that block’s inputs. Call these the block’s input constraints. 3. check each block’s inner assertions under its input constraints, using bounded model checking with satisfiability solving.

Incorporating Constraints: 

Incorporating Constraints 1. Formula (1) without constraints [[ M ]]k := I (s0)∧ (1) 2. Formula (2) with constraints [[ M ]]k := I (s0)∧c (s0)∧T (s0,s1)∧c (s1) ∧…∧T (sk-1,sk)∧c (sk) (2)

Safety Property Checking Procedure: 

Safety Property Checking Procedure 1. Check whether p is a combinational tautology in the unconstrained K, using formula 1. If it is, exit. 2. Check whether p is an inductive invariant for the unconstrained K, using formula 1. If it is, exit. 3. Check whether p is a combinational tautology in the presence of input constraints, using formula 2. If it is, go to step 6. 4. Check whether p is an inductive invariant in the presence of input constraints, using formula 2. It it is, go to step 6.

Safety Property Checking Procedure: 

Safety Property Checking Procedure 5. Check if a bounded length counterexample exists to AGp in the presence of input constraints, using formula 2. If one is found, there is no need to examine c, since the counterexample would exist without input constraints. If a counterexample is not found, go to step 6. The input constraints may need to be reformulated and this procedure repeated from step 3.

Safety Property Checking Procedure: 

Safety Property Checking Procedure 6. Check the input constraints, c. Inputs that are constrained in one design block, A, will, in general, be outputs of another design block, B. We turn them into inner assertions for B, and check them with the above procedure. Also circular reasoning can be deleted automatically.

Conclusions: 

Conclusions + Entails only slight memory and CPU usage. + Extremely fast for invariance checking. + Counterexamples and witnesses are of minimal length, which make them easy to understand. + Well to automation, needs little by-hand intervention. - Implementations are limited as to the types of properties that can be checked - No clear evidence that the technique will consistently find long counterexample or witnesses.

Directions for future research: 

Directions for future research 1. The use of domain knowledge to guide search in SAT procedures. 2. New technique for approaching completeness, especially in safety property checking, where it may be the most possible. 3. Combining bounded model checking with other reduction techniques 4. Combining bounded model checking with partial BDD approach.