Reliable Verification Using Symbolic Simulation with Scalar Values 

Chris Wilson and David L. Dill

Computer Systems Laboratory
Stanford University
Stanford, CA, 94035

chriswi@leland.stanford.edu
dill@cs.stanford.edu


This paper presents an algorithm for hardware verification that uses
simulation and satisfiability checking techniques to determine the
correctness of a symbolic test case on a circuit.  The goal is to have
coverage greater than that of random testing, but with the ease of use
and predictability of directed testing.  The user uses symbolic variables
in simple directed tests to increase the input space that is explored.
The algorithm, which is called {\em quasi-symbolic simulation}, simulates
these tests using only scalar (0,1,X) values internally causing potentially
conservative values to be generated at the outputs.  Divide and conquer
of the symbolic input space is used to resolve this conservativeness.
In the best case, this method is as efficient as symbolic simulation
using BDDs and, in the worst case, gives coverage and predictability at
least as good as directed testing.