Verified AIG Algorithms in ACL2
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...
Main Authors: | Jared Davis, Sol Swords |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2013-04-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1304.7861v1 |
Similar Items
-
A verified framework for symbolic execution in the ACL2 theorem prover
by: Swords, Sol Otis
Published: (2011) -
Bit-Blasting ACL2 Theorems
by: Sol Swords, et al.
Published: (2011-10-01) -
Hint Orchestration Using ACL2's Simplifier
by: Sol Swords
Published: (2018-10-01) -
Verifying Sierpiński and Riesel Numbers in ACL2
by: John R. Cowles, et al.
Published: (2011-10-01) -
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
by: Disha Puri, et al.
Published: (2014-06-01)