A SAT-based procedure for verifying finite state machines in ACL2

We describe a new procedure for verifying ACL2 properties about finite state machines (FSMs) using satisfiability (SAT) solving. We present an algorithm for converting ACL2 conjectures into conjunctive normal form (CNF), which we then output and check with an external satisfiability solver. The procedure is directly available as an ACL2 proof request. When the SAT tool is successful, a theorem is added to the ACL2 system database as a lemma for use in future proof attempts. When the SAT tool is unsuccessful, we use its output to construct a counter-example to the original ACL2 property. Categories and Subject Descriptors B.5.2 [Register-Transfer-Level Implementation]: Design Aids—Verification; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages—Decision problems; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Mechanical theorem proving, Recursive function theory General Terms verification, algorithms Keywords hardware verification, Satis�...

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Warren A. Hunt Jr., Erik Reeber
• Keywords: ACL2, ACL2 2006, Computational Linguistics, Original Acl2 Property, SAT Tool