Symbolic Verification of Systems with State Machines
Systems that combine finite state machines and data paths (including
register files, caches, and memories) can be difficult to verify. The
datapath and finite-state machines together are too large for model
checkers, and have too much random control behavior for practical
theorem-proving. Abstracting the datapath is not always easy
to do correctly, and the finite state machines are difficult
to specify without the attached datapath (the FSMs are correct
if they make the datapath do the right thing).
We have been working on a method to verify such systems by combining
regular expressions, symbolic simulation, and a decision procedures
for quantifier-free first-order logic. Regular expressions are
extracted from the FSMs that describe all paths between certain states
that are especially easy to specify (called "clean states"). A
symbolic simulator is used to simulate along all the paths described
by the regular expressions (using special approximations for loops).
Invariants are proved on the results of the symbolic simulation
using the decision procedure.
This method has been applied, with great effort, to two designs
created by other groups at Stanford: the instruction fetch unit from
the Torch microprocessor, and the load-store unit from the Protocol
Processor ("magic chip") of the Flash multiprocessor.
A preliminary paper on this was published in FMCAD '98.