Bit-Blasting ACL2 Theorems

TL;DR

This paper introduces a framework called GL that automates the process of proving finite ACL2 theorems using BDD and SAT reasoning, reducing human effort and speeding up verification.

Contribution

It presents a novel automation approach for ACL2 theorem proving by integrating BDD and SAT-based reasoning within the GL framework.

Findings

Successfully verified x86 execution units at Centaur Technology.

Automated theorem proving reduces manual guidance in ACL2.

Framework improves efficiency in verifying arithmetic properties.

Abstract

Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.