Explaining Counterexample Of Model Checking

The complexity of today's hardware designs has grown to a point where verification has become a major bottleneck. And verification designs with only dynamic simulation cannot guarantee a satisfy level of coverage. So formal verification is becoming more and more important in the design flows.Today, model checking is one of the most important formal verification approaches. It is widely employed to verify software and hardware system. One of its major advantages in comparison to such method as theorem proving is the production of a counterexample, which explains how the system violates some assertion.However, it is a tedious task to understand the complex counterexamples generated by model checker. A verification engineer often needs to check out thousands of evens and signals, before discover the real bug. Therefore, how to automatically extract useful information to aid the understanding of counterexample is an area of active research.At the same time, many important verification algorithms need to analysis counterexample (or witness). Some of them are: abstraction-refinement model checking and SAT based image computation. In these algorithms, if we can extract a small subset of variables that are sufficient to lead to counterexample, then these variables can express a large number of counterexamples, not just the individual one generated by model checker. Directly processing this variables subset can make these algorithm exponent faster than origin algorithm, which process the individual counterexample generated by model checker.So it is very important to process the counterexample according to varias special needs. We call these process approaches as Counterexample Explanation. It includes two categories approaches:1. Bug Localization: When the processed result need to be check out by a verification engineer, then it is important to keep the result as succinct as possilbe, and do not need to consider too much about the completeness and run time overhead.2. Counterexample Minimization: When the processed result need to be further processed by other algorithm (such as abstraction/refinement or SAT-based image computation), the completeness and run time overhead are very important.We deal with all these aspects in varias chapters of this thesis.1. To locate bug in counterexample more accurately, we improve existing nearest witness searching technique by iterativly witness searching. Our approach measures the distance between two state transition traces with difference of their control flow. With respect to this distance metrics, our approach search for a witness as near as possible to the counterexample. Then we can obtain the set of control flow predicates withdifference assignment in witness and counterexample. Run this witness-searching algorithm iteratively, we can then obtain a predicate list with priority. A predicate with higher priority means that this predicate is more likely the actual error. Experiment result shows that our approach is highly accurate.2. We propose an improved faster version of BFL algorithm-the most efficient complete counterexample minimization approach. Run time overhead of BFL is very large due to one call to SAT solver per candidate variable to be eliminated. So we propose a faster counterexample minimization algorithm based on refutation analysis. For every UNSAT instance of BFL, we perform refutation analysis to extract the set of variables that lead to UNSAT, all variables not belong to this set can be eliminated directly. In this way, we can eliminate many variables with only one call to SAT solver. At the same time, we propose a further improvement on BFL with incremental SAT. With incremental SAT approach, we can share conflict clauses between similar instance of BFL, and prevent overlapped state space from being searched repeatedly. In the way, we can achieve 1 to 2 orders of magnitude speedup over BFL.3. We propose a stepwise BFL algorithm, to reduce the space overhead of BFL. Given that we have reduced the run time overhead of BFL with refutation analysis, the space overhead remains the major difficulty faced by BFL. It is because of the full length unfolding of transition relation, which may cause memory overflow for deep counterexample of complex system model. To overcome this problem, our approach works backward from the cycle that violates the property, to the initial cycle. At each cycle, we extract a small subset of input and current state variables, which are sufficient to lead to assignment of the already minimized next state variable set. In this way, we only need to store a copy of transition relation in memory, instead of multiple copies as that of BFL. Experiment result shows that, our approach can significantly decrease the space and run time overhead with only minor lose in its counterexample minimization ability.4. We propose a counterexample minimization algorithm for invariant of nondeterministic system. Many complex systems can only be modeled as nondeterministic system. Their counterexample can't be minimized by existing approaches, which are designed for deterministic systems. Therefore, we propose a novel counterexample minimization approach for nondeterministic system. For each certain cycle of a counterexample, our approach tries to find a state set, which can be represented as a succinct cube. Starting from every state in such cubes, there must exist a path that runs through cubes of following cycles and lead to property violation at last. We formulate this problem as a sequence of pre-image computations, and then employ an efficient SAT-based approach to compute these pre-images. Experiment result shows that, our approach can significantly minimize counterexample of nondeterministic system.5. We proposes a novel approach to minimize counterexample of general Kripke structureand ACTL property, while existing approach can only minimize path-like counterexample of invariant property. The major issue of this algorithm is how to minimize loop in loop-like counterexample. For such a loop, we try to enlarge it to a sequence of succinct cube, such that for every state of every certain cube in this sequence, there must exist a valid loop, which run through this state and all other cubes. This enlargement operation is formulated as a sequence of guided pre-image computations, which yields a fixpoint at last. Experiment result shows that our algorithm can significantly reduce the size of counterexample of ACTL property. 6. Based on all above work, we extend the NuSMV model cheker and Zchaff SAT solver, to design an automatic tool environment, which can automaticly locate bug and minimizing complex counterexample.