		Search-engine friendly clone of the ACL2 documentation.

Aignet-transforms

Aignet-comb-transforms

Aignet transforms that simplify the network while preserving combinational equivalence

The functions apply-comb-transforms and apply-comb-transforms! may be used to apply several transforms to an aignet network, each of which preserves combinational equivalence with the original network. The transforms are chosen by listing several comb-transform objects, each of which is a configuration object for one of the supported transforms. The currently supported transforms are:

An additional "transform" that simply writes a snapshot of the network to an aiger file is also supported.

Subtopics

Fraig: Apply combinational SAT sweeping (fraiging) to remove redundancies in the input network.
Parametrize: Transform the AIG so that some conditions assumed to be untrue don't affect the logical equivalence of nodes, using BDDs to compute a hopefully-efficient parametrization.
Observability-fix: Transform the aignet so that some observability don't-care conditions don't affect the logical equivalence of nodes.
Constprop: Simplify a single-output aignet by assuming inputs from a top-level conjunction to be true.
Apply-m-assumption-n-output-output-transform-default
Balance: Apply DAG-aware AND tree balancing to the network.
Apply-n-output-comb-transform-default
Apply-comb-transform-default
Obs-constprop: Combine constprop and observability-fix for a transform that is sometimes somewhat better than simply running both in sequence.
Rewrite: Apply DAG-aware rewriting to the network.
Comb-transform: Configuration object for any combinational transform supported by apply-comb-transforms.
Abc-comb-simplify: Use the external tool ABC to apply a combinational simplification to the network, and assume the result correct.
Prune: Apply combinational pruning to remove unused nodes in the input network.
Rewrite!: Apply DAG-aware rewriting to the network.
M-assumption-n-output-comb-transform->name
N-output-comb-transform->name
Comb-transform->name
N-output-comb-transformlist: A list of n-output-comb-transform-p objects.
M-assumption-n-output-comb-transformlist: A list of m-assumption-n-output-comb-transform-p objects.
Comb-transformlist: A list of comb-transform-p objects.
Apply-comb-transform: Stub for an AIG transform that preserves combinational equivalence