## A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)

### Warren A. Hunt, Jr. and Erik Reeber

### The University of Texas

We define the Subclass of Unrollable List Formulas in ACL2 (SULFA).
SULFA is a subclass of ACL2 formulas based on list structures
that is sufficiently expressive to include invariants of
finite state machines (FSMs).
We have extended the ACL2 theorem prover to include a
new proof mechanism, which can recognize SULFA formulas and
automatically verify them with a SAT-based decision procedure.
When this decision procedure is successful, a theorem is added
to the ACL2 system database as a lemma for use
in future proof attempts. When unsuccessful, a counter-example to the
SULFA property is presented.
We are using SULFA and its SAT-based decision procedure as part
of a larger system to verify components of the TRIPS processor.
Our verification system translates Verilog designs automatically
into ACL2 models. These models are written such that their invariants
are SULFA properties, which can be verified by our SAT-based
decision procedure, traditional theorem proving, or a
mixture of the two.