Verified AIG Algorithms in ACL2
The work
| Authors | Jared Davis; Sol Swords |
|---|---|
| Editors | |
| Type | article |
| Year | 2013 |
| Citekey | davis2013verified |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Publisher | Open Publishing Association |
| Volume | 114 |
| Pages | 95--110 |
Identifiers
| arXiv | 1304.7861 |
|---|---|
| DOI | 10.4204/eptcs.114.8 |
| ISSN | 2075-2180 |
Access
| Landing page | https://doi.org/10.4204/eptcs.114.8 |
|---|---|
| Free full text | https://arxiv.org/pdf/1304.7861 |
Related
| Distinct from | andrici2019verifying |
|---|---|
| Distinct from | biere1999symbolic |
| Distinct from | bouzafour2018modelchecking |
| Distinct from | bryant1986graphbased |
| Distinct from | bryant2021dual |
| Distinct from | claessen2009faithful |
| Distinct from | dumitrescu2003construction |
| Distinct from | hunt1994fm8501 |
| Distinct from | mishchenko2005fraigs |
| Distinct from | nukala2024translating |
| Distinct from | swords2011bitblasting |
| Distinct from | toma2006verification |
| Distinct from | yang2025forword |
| Distinct from | yu2025fraigbmc |
From crossref.
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.
A copy is held
pdf, 284.1 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-16 16:22 UTC |
| Approved by | a person 2026-09-16 20:49 UTC |
Cite it as
@article{davis2013verified,
title = {Verified AIG Algorithms in ACL2},
author = {Jared Davis and Sol Swords},
year = {2013},
journal = {Electronic Proceedings in Theoretical Computer Science},
publisher = {Open Publishing Association},
volume = {114},
pages = {95--110},
issn = {2075-2180},
eprint = {1304.7861},
doi = {10.4204/eptcs.114.8},
}
This record lives at https://refs.drheap.org/davis2013verified/ and will keep doing so.