Computer Science Department
School of Computer Science, Carnegie Mellon University
Experiments with SAT-Based Symbolic Simulation
Using Reparameterization in the Abstraction
Pankaj Chauhan, Edmund Clarke, Daniel Kroening
Keywords: Symbolic simulation, counterexample guided abstraction
refinement (CEGAR), parametric representation, reparameterization,
SAT Checkers, bounded model checking
This paper presents experimental results on the performance effect
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 model used for the BMC
instance is not abstracted, and thus is susceptible to the state
space explosion problem. We address this issue by using a symbolic
simulator with a SAT-based reparametrization algorithm as a
replacement for BMC within the abstraction refinement framework.
The reparametrization is performed as soon as the equations
maintained by the symbolic simulator become too large. We discuss
the quality of the refinement information that is extracted from
the symbolic simulator.