| |
|
|
Symbolic Verification of Systems with State Machines
AbstractSystems 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. See http://verify.stanford.edu/PAPERS/SDS98.ps Presentation Slides |