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.