Experiments With SAT-Based Symbolic Simulation Using Reparameterization in the Abstraction Refinement Framework
- Topics:
- Electrical and Electronic
- Tags:
- Abstraction Refinement,
- Abstraction Refinement Framework,
- Carnegie-Mellon University,
- Engineering,
- Human Resources,
- Performance Management,
- Workforce Management
- Source:
- Carnegie Mellon University
FREE Registration is required
Overview: This white paper presents experimental results on the performance of using symbolic simulation with SAT-based reparametrization within the Counterexample Guided Abstraction Refinement framework. Abstraction refinement has been applied successfully to prove safety properties of large industrial circuits. However, all existing abstraction refinement frameworks simply use SAT-based Bounded Model Checking (BMC) to refute the property. The paper addresses this issue by using a symbolic simulator with a SAT-based reparametrization algorithm as a replacement for BMC within the abstraction refinement framework.
(Is this item miscategorized? Does it need more tags? Let us know.)
Format: PDF | Size: 160KB | Date: May 2004 | Pages: 19



