Abstraction Refinement for Large Scale Model Checking

1. Front Matter

   Pages i-xiv

   PDF

2. Introduction

   Pages 1-10

3. Symbolic Model Checking

   Pages 11-40

4. Abstraction

   Pages 41-54

5. Refinement

   Pages 55-83

6. Compositional SCC Analysis

   Pages 85-100

7. Disjunctive Decomposition

   Pages 101-119

8. Far Side Image Computation

   Pages 121-135

9. Refining SAT Decision Ordering

   Pages 137-152

10. Conclusions

    Pages 153-156

11. Back Matter

    Pages 157-179

    PDF

Abstraction Refinement for Large Scale Model Checking summarizes recent research on abstraction techniques for model checking large digital system. Considering both the size of today's digital systems and the capacity of state-of-the-art verification algorithms, abstraction is the only viable solution for the successful application of model checking techniques to industrial-scale designs. This book describes recent research developments in automatic abstraction refinement techniques. The suite of algorithms presented in this book has demonstrated significant improvement over prior art; some of them have already been adopted by the EDA companies in their commercial/in-house verification tools.

• Abstraction Refinement
• Hachtel
• Integrated Circuits
• Large Scale Model Checking
• Somenzi
• Wang
• algorithms
• model

• NEC Laboratories America, Princeton, USA

  Chao Wang

• Department of Electrical/Computer Engineering, University of Colorado, Boulder, USA

  Gary D. Hachtel, Fabio Somenzi

Policies and ethics