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,

: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 , ornil ), 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 , ornil ), 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.