Sciweavers

DAC
2004
ACM

A SAT-based algorithm for reparameterization in symbolic simulation

14 years 4 months ago
A SAT-based algorithm for reparameterization in symbolic simulation
Parametric representations used for symbolic simulation of circuits usually use BDDs. After a few steps of symbolic simulation, state set representation is converted from one parametric representation to another smaller representation, in a process called reparameterization. For large circuits, the reparametrization step often results in a blowup of BDDs and is expensive due to a large number of quantifications of input variables involved. Efficient SAT solvers have been applied successfully for many verification problems. This paper presents a novel SAT-based reparameterization algorithm that is largely immune to the large number of input variables that need to be quantified. We show experimental results on large industrial circuits and compare our new algorithm to both SAT-based Bounded Model Checking and BDD based symbolic simulation. We were able to achieve on average 3x improvement in time and space over BMC and able to complete many examples that BDD based approach could not eve...
Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2004
Where DAC
Authors Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening
Comments (0)