Rewriting for Symbolic Execution of State Machine Models

J Strother Moore
Computer Science Department
University of Texas at Austin
email: moore@cs.utexas.edu

Abstract

We describe an algorithm for simplifying a class of symbolic expressions that arises in the symbolic execution of formal state machine models. These expressions are compositions of state access and change functions and if-then-else expressions, laced together with local variable bindings (e.g., lambda applications). The algorithm may be used in a stand-alone way, but is designed to be part of a larger system employing a mix of other strategies. The algorithm generalizes to a rewriting algorithm that can be characterized as outside-in or lazy, with respect both to variable instantiation and equality replacement. The algorithm exploits memoization or caching.

Keywords

hardware modeling, verification, microprocessor simulation, theorem proving, pipelined machine

Final CAV 01 Paper

Addendum to CAV 01 Paper

Simple Test Suite

J Strother Moore
December, 2000