\begin{abstract}
Symbolic methods such as model checking using binary decision diagrams
(BDDs) have had limited success in verifying large designs
because BDD sizes regularly exceed memory capacity.
Symbolic simulation is a method that controls BDD size by allowing
the user to specify the number of symbolic variables in a test.
However, BDDs still may blow up when using symbolic simulation in large designs
with a large number of symbolic variables.
This paper describes techniques for
limiting the size of the internal representation of values in symbolic
simulation no matter how many symbolic variables are present.
The basic idea is to use approximate values on internal nodes;
an approximate
value is one that consists of combinations of the values $0$, $1$, and
$X$. If an internal node is known not to affect the functionality being
tested, then the simulator can output a value of $X$ for this node, reducing the
amount of time and memory required to represent the value of this node.
Our algorithm uses categorization of the symbolic input variables to
determine which node values can be more approximate and which can be more exact.
\end{abstract}