Aignet-abc
Run abc on an aignet, with a few different possible axioms about what comes out.
This function is identical to aignet-run-abc-core, but takes
one additional keyword argument, axiom. This argument specifies what can
be assumed about the results. The soundness of this assumption is highly
questionable and dependent on the soundness of ABC and the appropriateness of
the script it is run with. The axiom may be any of the following; if it is
anything else or is not specified, then nothing particular is assumed.
- :comb-prove: Asserts that if we produce :proved as the status, it
implies that all outputs and register nextstates of the input AIG are
combinationally constant-true; that is, for any setting of the inputs and
register states.
- :comb-simp Asserts that if we produce a non-error status (one of
:proved, :refuted, :failed, or nil), and the output
filename was given, that the output aignet is combinationally equivalent to the
input aignet (see comb-equiv).
- :comb-prove-simp combines the assertions of :comb-prove and
:comb-simp.
- :seq-prove: Asserts that if we produce :proved as the status, it
implies that all outputs of the input AIG are sequentially constant-true
starting from the all-0 initial state.
- :seq-simp Asserts that if we produce a non-error status (one of
:proved, :refuted, :failed, or nil), and the output
filename was given, that the output aignet is sequentially equivalent to the
input aignet (see seq-equiv).
- :seq-prove-simp combines the assertions of :seq-prove and
:seq-simp.
See abc-example-scripts for example scripts that may be appropriate
for these various assumptions, modulo the correctness of ABC.
