Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Ipasir
Aignet
Base-api
Aignet-construction
Representation
Aignet-copy-init
Aignet-simplify-with-tracking
Aignet-simplify-marked-with-tracking
Aignet-cnf
Aignet-simplify-marked
Aignet-complete-copy
Aignet-transforms
Aignet-eval
Semantics
Aignet-read-aiger
Aignet-write-aiger
Aignet-abc-interface
Aignet-run-abc-core
Aignet-run-abc-core-st
Aignet-abc
Abc-example-scripts
Utilities
Aig
Satlink
Truth
Ubdds
Bdd
Faig
Bed
4v
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Aignet
Aignet-abc-interface
Using the open-source synthesis and equivalence/model-checking tool ABC with aignet
Subtopics
Aignet-run-abc-core
Run abc on an aignet, without using state
Aignet-run-abc-core-st
Run abc on an aignet; takes and returns state.
Aignet-abc
Run abc on an aignet, with a few different possible axioms about what comes out.
Abc-example-scripts
Example scripts to use with
aignet-abc
.