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.
