Predicate Abstraction and Refinement Techniques for Verifying Verilog
Abstract
Model checking techniques applied to large industrial circuits suffer from the state explosion problem. A major technique to address this problem is abstraction. Predicate abstraction has been applied successfully to large software programs. Applying this technique to hardware designs poses additional challenges. This paper evaluates three techniques to improve the performance of SAT-based predicate abstraction of circuits: (1) We partition the abstraction problem by forming subsets of the predicates. The resulting abstractions are more coarse, but the computation of the abstract transition relation becomes easier. (2) We evaluate the performance effect of lazy abstraction, i.e., the abstraction is only performed if required by a spurious counterexample. (3) We use weakest preconditions of circuit transitions in order to obtain new predicates during refinement. We provide experimental results on publicly available benchmarks from the Texas97 benchmark suite.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 25, 2004
- Accession Number
- ADA457877
Entities
People
- Daniel Kroening
- Edmund M. Clarke
- Himanshu Jain
Organizations
- Carnegie Mellon University