Existing formal verification methods do not handle systems that
combine state machines and data paths very well.
Model checking deals with finite-state machines efficiently,
but model checking full designs is infeasible because of the
large amount of state in the data path.
Theorem-proving methods may be effective for verifying data
path operations, but verifying the control
requires finding and proving
inductive invariants that
characterize the reachable states of the system.
We present a new approach to verification of systems that combine
control FSMs and data path operations.
Invariants are specified only for a small set of control states,
called {\em clean states}, where the invariants are especially
simple. We avoid the need to specify the invariants
for the unclean states by symbolically simulating over all paths
to find the possible next clean states.
The set of all paths from one clean state to the next is represented
by a regular expression, which is extracted from the control FSMs.
The number of paths is infinite only if the regular expression
contains stars. The method uses a heuristic to generalize the
symbolic state to cover all of the paths of the starred expression.
We have implemented a prototype tool for guiding an existing symbolic
simulator and verification tool and used it successfully to prove
properties of the Instruction Fetch Unit of TORCH, a superscalar
microprocessor designed at Stanford. With much less effort, we
were able to find all the bugs in the unit that were found earlier
by manually strengthening the invariants.