# 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