Predicate Abstraction and Refinement Techniques for Verifying Verilog
- Topics:
- Electrical and Electronic
- Tags:
- Abstraction,
- Human Resources,
- Performance Management,
- Productivity,
- Technique,
- Workforce Management
- Source:
- Carnegie Mellon University
FREE Registration is required
Overview: This white paper evaluates three techniques to improve the performance of SAT-based predicate abstraction of circuits. First the partition of the abstraction problem by forming subsets of the predicates making the resulting abstractions more coarse, but the computation of the abstract transition relation becomes easier, secondly evaluates the performance effect of lazy abstraction, i.e., the abstraction is only performed if required by a spurious counterexample and lastly uses weakest preconditions of circuit transitions in order to obtain new predicates during refinement.
(Is this item miscategorized? Does it need more tags? Let us know.)
Format: PDF | Size: 170KB | Date: Jun 2004 | Pages: 26
