Verified AIG Algorithms in ACL2

TL;DR

This paper introduces verified AIG representations within ACL2, enabling formal reasoning about AIG algorithms and integrating SAT solvers for improved hardware verification in a theorem prover.

Contribution

It develops two verified AIG representations in ACL2, along with conversion and reasoning tools, bridging AIG algorithms with formal verification and SAT solving.

Findings

Verified AIG representations in ACL2 implemented.

Conversion and reasoning strategies for AIG algorithms developed.

Practical integration of SAT solvers for ACL2 theorem proving.

Abstract

And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches. We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms. Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance.