Loading...
Please wait, while we are loading the content...
Similar Documents
Automatic Abstraction in Model Checking (2000)
| Content Provider | CiteSeerX |
|---|---|
| Author | Lu, Yuan |
| Abstract | As technology advances and demand for higher performance increases hardware designs are becoming more and more sophisticated. A typical chip design may contain over ten million switching devices. Since the systems become more and more complex, detecting design errors for systems of such scale becomes extremely difficult. Formal verification methodologies can potentially catch subtle design errors. However, many state-of-the-art formal verification tools suffer from the state explosion problem. This thesis explores abstraction techniques to avoid the state explosion problem. In our methodology, atomic formulas extracted from an SMV-like concurrent program are used to construct abstraction functions. The initial abstract structure is built by using existential abstraction techniques. When the model checker disproves a universal property on the abstract structure, it generates a counterexample. However, this abstract counterexample might be spurious because abstraction is not complete. We provide a new symbolic algorithm to determine whether an abstract counterexample is spurious. When a counterexample is identified to be spurious, the algorithm will compute the shortest prefix of the abstract counterexample that does not correspond to an actual trace in the concrete model. The last abstract state in this prefix is split into less abstract states so that the spurious counterexample is eliminated. Thus, a more refined abstraction function is obtained. It is usually desirable to obtain the coarsest refinement which eliminates the counterexample because this corresponds to the smallest abstract model that avoids the spurious counterexample. We prove, however, that finding the coarsest refinement is NP-hard. Because of this, we use a polynomial-time algorithm which gives a su... |
| File Format | |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | Abstract State Many State-of-the-art Formal Verification Tool Subtle Design Error Model Checker Initial Abstract Structure Abstraction Function Abstract Structure Actual Trace Model Checking Refined Abstraction Function Formal Verification Methodology Abstract Model Abstract Counterexample Atomic Formula Typical Chip Design Technology Advance Spurious Counterexample State Explosion Problem Existential Abstraction Technique Performance Increase Abstraction Technique Scale Becomes Polynomial-time Algorithm Universal Property Smv-like Concurrent Program Concrete Model Automatic Abstraction Design Error Last Abstract State New Symbolic Algorithm |
| Content Type | Text |
| Resource Type | Article |
