Reliable Symbolic Simulation Using Scalar Values and BDDs

Chris Wilson David L. Dill

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Symbolic simulation has the potential to improve upon primary verification methods such as directed and random testing. However, traditional BDD-based symbolic simulation can have unpredictable memory blow-up making it too unreliable to be used as a primary verification method. One way of making symbolic simulation more reliable is to use scalar values, which require only constant memory, to approximate values on nodes. Exact values can be generated when necessary by alternately setting the value of a selected variable to the constants $0$ and $1$ and re-running the simulation with these constants. This paper introduces BDD based approximations into this process to make values more exact where necessary to reduce the amount of re-simulation required. The result of this is that performance can be improved compared to using scalar values alone while maintaining the reliability needed for mainstream verification.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems