aigverse.abc.gia¶

The ABC9 (&-space) commands, run on ABC’s GIA store.

ABC keeps two independent network stores and a command only ever sees its own. The functions in aigverse.abc operate on the classic store; the ones here operate on the GIA, and transfer the network with &read/&write rather than read_aiger/write_aiger.

They are reached through the gia namespace, which mirrors ABC’s own & prefix:

from aigverse import abc

optimized = abc.gia.dc2(aig)  # ABC's `&dc2`
optimized = abc.dc2(aig)  # ABC's `dc2`, a different command

The &-space is not a mirror of the classic command set. There is no &rewrite and no &refactor; &dc2 is the heavy-rewriting equivalent, and &syn2/&syn3/&syn4 are composite scripts rather than single commands. What the &-space adds is a genuinely different optimization strategy: these commands map to LUTs internally and unmap again, which restructures far more aggressively than the classic commands do.

These are aimed at depth rather than area, but whether they deliver is strongly design-dependent and worth measuring rather than assuming. On a 4-bit ripple-carry multiplier, &syn4 trades 84 gates at 16 levels for 168 gates at 13 levels – depth the classic scripts cannot reach on that design. On a 16-bit carry-lookahead adder the same command buys nothing: it grows the network and leaves the depth where it was, while resyn2 beats it on both counts. Neither family dominates.

The & space is also stricter than the classic one about register reset values. &read accepts only a reset of 0 literally: it converts a 1-valued flip-flop by complementing it, which is an equivalent network that comes back with a reset of 0, and it models an undefined reset with an extra primary input, an extra register, and three AND nodes – a network with a different interface than it went in with. The first is carried, the second is refused with a ValueError by every function here. The classic store keeps either reset value as it is.

Module Contents¶

class CecStatus(*args, **kwds)[source]¶

Bases: enum.Enum

The outcome of an equivalence check.

Deliberately not usable as a boolean: if cec(a, b): would read as “equivalent” while quietly also firing for UNDECIDED and TIMEOUT, which are not the same claim at all. Compare explicitly:

if abc.gia.cec(a, b) is abc.gia.CecStatus.EQUIVALENT:
    ...

EQUIVALENT = 'equivalent'¶

NOT_EQUIVALENT = 'not equivalent'¶

UNDECIDED = 'undecided'¶

TIMEOUT = 'timeout'¶

__bool__() → bool[source]¶

Refuses truth testing.

Raises:: TypeError – Always. Compare against a member instead.

class Balance[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &b command on a network, or builds it as a command.

static cmd(*, delay_only: bool = False, and_only: bool = False, strict_area: bool = False, max_fanout: int | None = None) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &b command without running it.

Parameters:

delay_only – If True, balance for delay without regard to area.
and_only – If True, use only AND nodes instead of AND/XOR/MUX.
strict_area – If True, control area strictly while balancing for delay. Only has an effect together with delay_only.
max_fanout – Fanout count above which a divisor is skipped (ABC’s -N, at least 0), or None for ABC’s default. Lowering it keeps the command away from high-fanout nodes.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If max_fanout is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, delay_only: bool = False, and_only: bool = False, strict_area: bool = False, max_fanout: int | None = None, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &b command on a network.

The &-space counterpart of balance. Unlike the classic command it understands XOR and MUX structures, so it can restructure where the classic one only re-associates AND trees.

Parameters:

ntk – The network to optimize.
delay_only – If True, balance for delay without regard to area.
and_only – If True, use only AND nodes instead of AND/XOR/MUX.
strict_area – If True, control area strictly while balancing for delay. Only has an effect together with delay_only.
max_fanout – Fanout count above which a divisor is skipped (ABC’s -N, at least 0), or None for ABC’s default. Lowering it keeps the command away from high-fanout nodes.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If max_fanout is outside the range ABC accepts.

balance: Final[Balance]¶: Runs ABC’s &b command on a network, or builds it as a command; see Balance.

class Resub[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &resub command on a network, or builds it as a command.

static cmd(*, max_inserts: int | None = None, max_support: int | None = None, max_divisors: int | None = None) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &resub command without running it.

Parameters:

max_inserts – Limit on the number of nodes added (ABC’s -N, at least 0), or None for ABC’s default.
max_support – Limit on the support size (ABC’s -S, at least 1), or None for ABC’s default.
max_divisors – Limit on the divisor count (ABC’s -D, at least 1), or None for ABC’s default.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If a limit is outside the range ABC accepts.

Runs ABC’s &resub command on a network.

The &-space counterpart of resub.

Parameters:

ntk – The network to optimize.
max_inserts – Limit on the number of nodes added (ABC’s -N, at least 0), or None for ABC’s default.
max_support – Limit on the support size (ABC’s -S, at least 1), or None for ABC’s default.
max_divisors – Limit on the divisor count (ABC’s -D, at least 1), or None for ABC’s default.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If a limit is outside the range ABC accepts.

resub: Final[Resub]¶: Runs ABC’s &resub command on a network, or builds it as a command; see Resub.

class Dc2[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &dc2 command on a network, or builds it as a command.

static cmd(*, update_levels: bool = True) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &dc2 command without running it.

Parameters:: update_levels – If True (ABC’s default), track levels while rewriting.
Returns:: The command, ready for run_script or run_many.

__call__(ntk: aigverse.abc._runner.AigT, *, update_levels: bool = True, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &dc2 command on a network.

Heavy rewriting, and the closest &-space equivalent of rewrite and refactor – neither of which has a direct & counterpart.

Parameters:

ntk – The network to optimize.
update_levels – If True (ABC’s default), track levels while rewriting.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

dc2: Final[Dc2]¶: Runs ABC’s &dc2 command on a network, or builds it as a command; see Dc2.

class Syn2[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &syn2 script on a network, or builds it as a command.

static cmd(*, delay_relaxation: int | None = None, cut_minimization: bool = False, delay_optimization: bool = False, coarsen: bool = True, old_algorithm: bool = False) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &syn2 command without running it.

Parameters:

delay_relaxation – Delay relaxation ratio (ABC’s -R, at least 0), or None for ABC’s default of 20. Higher values allow more delay in exchange for area.
cut_minimization – If True, enable cut minimization.
delay_optimization – If True, run the additional delay optimization.
coarsen – If True (ABC’s default), coarsen the subject graph before mapping, which gives the mapper larger cuts to work with.
old_algorithm – If True, use ABC’s previous implementation instead of the current one.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If delay_relaxation is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, delay_relaxation: int | None = None, cut_minimization: bool = False, delay_optimization: bool = False, coarsen: bool = True, old_algorithm: bool = False, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &syn2 script on a network.

The lightest of the three & synthesis scripts.

Warning

These scripts buy depth with area, and they spend it whether or not there is depth to be had. On a design where they find none, the AND count grows and nothing comes back for it – a 16-bit carry-lookahead adder goes from 186 gates to 698 under &syn2 here. That is ABC behaving as designed, not a failure; compare the result before keeping it.

Parameters:

ntk – The network to optimize.
delay_relaxation – Delay relaxation ratio (ABC’s -R, at least 0), or None for ABC’s default of 20. Higher values allow more delay in exchange for area.
cut_minimization – If True, enable cut minimization.
delay_optimization – If True, run the additional delay optimization.
coarsen – If True (ABC’s default), coarsen the subject graph before mapping, which gives the mapper larger cuts to work with.
old_algorithm – If True, use ABC’s previous implementation instead of the current one.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If delay_relaxation is outside the range ABC accepts.

syn2: Final[Syn2]¶: Runs ABC’s &syn2 script on a network, or builds it as a command; see Syn2.

class Syn3[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &syn3 script on a network, or builds it as a command.

static cmd() → aigverse.abc._runner.Command[source]¶

Builds ABC’s &syn3 command without running it.

Returns:: The command, ready for run_script or run_many.

__call__(ntk: aigverse.abc._runner.AigT, *, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &syn3 script on a network.

A different restructuring schedule from syn2; which of the two wins is design-dependent, so both are worth trying.

Warning

Like syn2, this trades area for depth and will grow the network on designs where there is no depth to recover.

Parameters:

ntk – The network to optimize.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

syn3: Final[Syn3]¶: Runs ABC’s &syn3 script on a network, or builds it as a command; see Syn3.

class Syn4[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &syn4 script on a network, or builds it as a command.

static cmd() → aigverse.abc._runner.Command[source]¶

Builds ABC’s &syn4 command without running it.

Returns:: The command, ready for run_script or run_many.

__call__(ntk: aigverse.abc._runner.AigT, *, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &syn4 script on a network.

The most aggressive of the three, and the one that spends the most area to buy depth.

Warning

Like syn2, this trades area for depth, and it spends the most of the three. Expect the AND count to grow, sometimes considerably.

Parameters:

ntk – The network to optimize.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

syn4: Final[Syn4]¶: Runs ABC’s &syn4 script on a network, or builds it as a command; see Syn4.

class Fraig[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &fraig command on a network, or builds it as a command.

static cmd(*, conflict_limit: int | None = None) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &fraig command without running it.

Parameters:: conflict_limit – Maximum SAT conflicts per node (ABC’s -C, at least 0), or None for ABC’s default. Lower values bound the runtime on hard instances at the cost of missing some merges. It is the only one of &fraig’s two dozen switches wrapped here; the rest tune the SAT sweeper internally and are reachable through run_script().
Returns:: The command, ready for run_script or run_many.
Raises:: ValueError – If conflict_limit is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, conflict_limit: int | None = None, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &fraig command on a network.

Combinational SAT sweeping: proves internal nodes functionally equivalent and merges them. This removes redundancy that no amount of structural rewriting can see, which makes it a good final pass – and a good one to run between two structural scripts that each introduced their own duplicates.

Parameters:

ntk – The network to optimize.
conflict_limit – Maximum SAT conflicts per node (ABC’s -C, at least 0), or None for ABC’s default. Lower values bound the runtime on hard instances at the cost of missing some merges. It is the only one of &fraig’s two dozen switches wrapped here; the rest tune the SAT sweeper internally and are reachable through run_script().
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If conflict_limit is outside the range ABC accepts.

fraig: Final[Fraig]¶: Runs ABC’s &fraig command on a network, or builds it as a command; see Fraig.

class Deepsyn[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &deepsyn command on a network, or builds it as a command.

static cmd(*, timeout: float | None = None, iterations: int | None = None, patience: int | None = None, stop_at_nodes: int | None = None, seed: int | None = None, two_input_luts: bool = False, optimize: bool = False) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &deepsyn command without running it.

Unlike the single-pass commands, timeout is a switch here: it is the budget ABC enforces itself (-T), so it belongs to the command and survives into a batch. What does not survive is the process backstop that deepsyn adds on top of it, so give a batch a timeout of its own for the case where ABC ignores its own budget.

Parameters:

timeout – Seconds ABC may spend searching (ABC’s -T), or None for no limit. Strongly recommended.
iterations – Number of search iterations (ABC’s -I, at least 1), or None for ABC’s default of 1.
patience – Number of steps without improvement after which the search gives up (ABC’s -J, at least 1), or None for ABC’s default, which is effectively unlimited.
stop_at_nodes – Stop once the network is this small (ABC’s -A), or None for no such limit.
seed – Random seed (ABC’s -S, 0 to 100), or None for ABC’s default.
two_input_luts – If True, search over two-input LUTs.
optimize – If True, enable ABC’s additional optimization step.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If an option is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, timeout: float | None = None, iterations: int | None = None, patience: int | None = None, stop_at_nodes: int | None = None, seed: int | None = None, two_input_luts: bool = False, optimize: bool = False, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &deepsyn command on a network.

A search rather than a pass: it repeatedly restructures the network with randomized parameters and keeps whatever came out smallest. That makes it the strongest thing in this module and also the slowest, and it means two runs with different seed values can give different results.

Give it a budget. Unlike the single-pass commands, timeout here is handed to ABC as its own internal limit, so ABC stops cleanly and returns the best result it has found rather than being killed with nothing to show.

ABC’s -c switch, which computes structural choices, is deliberately not exposed: it leaves an AIG with choices in the GIA store, which &write cannot serialize – ABC aborts on an internal assertion rather than reporting an error, so the result could never come back across the bridge.

Parameters:

ntk – The network to optimize.
timeout – Seconds ABC may spend searching (ABC’s -T), or None for no limit. Strongly recommended.
iterations – Number of search iterations (ABC’s -I, at least 1), or None for ABC’s default of 1.
patience – Number of steps without improvement after which the search gives up (ABC’s -J, at least 1), or None for ABC’s default, which is effectively unlimited.
stop_at_nodes – Stop once the network is this small (ABC’s -A), or None for no such limit.
seed – Random seed (ABC’s -S, 0 to 100), or None for ABC’s default.
two_input_luts – If True, search over two-input LUTs.
optimize – If True, enable ABC’s additional optimization step.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If an option is outside the range ABC accepts.

deepsyn: Final[Deepsyn]¶: Runs ABC’s &deepsyn command on a network, or builds it as a command; see Deepsyn.

class Transduction[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &transduction command on a network, or builds it as a command.

static cmd(*, transduction_type: int | None = None, fanin_sort: int | None = None, script_parameters: int | None = None, seed: int | None = None, randomize_seed: int | None = None, truth_tables: bool = False, mspf: bool = False, preserve_levels: bool = False) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &transduction command without running it.

Parameters:

transduction_type – Which variant to run (ABC’s -T, 0 to 8), or None for ABC’s default of 1 (Resub). Types 6 to 8 are the repeat scripts and are considerably more expensive.
fanin_sort – Order in which fanins are visited (ABC’s -S, 0 to 4), or None for ABC’s default of 0 (topological). The order decides which of several valid reductions is found first.
script_parameters – Parameters for the repeat scripts (ABC’s -P, at least 0), or None for ABC’s default of 0. Only meaningful for transduction_type 6 to 8.
seed – Seed used to shuffle the inputs (ABC’s -I), or None not to shuffle. Different seeds explore different results.
randomize_seed – Seed from which all parameters are drawn at random (ABC’s -R), or None to use the parameters as given. Setting it overrides the individual choices above.
truth_tables – If True, reason with truth tables instead of BDDs, which is faster on small functions and infeasible on wide ones.
mspf – If True, use maximum set of permissible functions instead of compatible ones. Stronger and more expensive.
preserve_levels – If True, do not increase the depth. ABC’s default here is False, unlike the classic commands.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If an option is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, transduction_type: int | None = None, fanin_sort: int | None = None, script_parameters: int | None = None, seed: int | None = None, randomize_seed: int | None = None, truth_tables: bool = False, mspf: bool = False, preserve_levels: bool = False, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &transduction command on a network.

Transduction reasons about permissible functions node by node, so it finds redundancy that structural rewriting cannot. It is BDD-based and its cost grows steeply with the network, so it is realistically limited to small designs – treat a few thousand AND nodes as the upper end and pass a timeout.

ABC offers no internal budget for this command, so timeout kills the process and yields nothing.

Contributed to ABC by Yukio Miyasaka.

Parameters:

ntk – The network to optimize.
transduction_type – Which variant to run (ABC’s -T, 0 to 8), or None for ABC’s default of 1 (Resub). Types 6 to 8 are the repeat scripts and are considerably more expensive.
fanin_sort – Order in which fanins are visited (ABC’s -S, 0 to 4), or None for ABC’s default of 0 (topological). The order decides which of several valid reductions is found first.
script_parameters – Parameters for the repeat scripts (ABC’s -P, at least 0), or None for ABC’s default of 0. Only meaningful for transduction_type 6 to 8.
seed – Seed used to shuffle the inputs (ABC’s -I), or None not to shuffle. Different seeds explore different results.
randomize_seed – Seed from which all parameters are drawn at random (ABC’s -R), or None to use the parameters as given. Setting it overrides the individual choices above.
truth_tables – If True, reason with truth tables instead of BDDs, which is faster on small functions and infeasible on wide ones.
mspf – If True, use maximum set of permissible functions instead of compatible ones. Stronger and more expensive.
preserve_levels – If True, do not increase the depth. ABC’s default here is False, unlike the classic commands.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If an option is outside the range ABC accepts.

transduction: Final[Transduction]¶: Runs ABC’s &transduction command on a network, or builds it as a command; see Transduction.

class Transtoch[source]¶

Bases: aigverse.abc._runner.CommandWrapper

Runs ABC’s &transtoch command on a network, or builds it as a command.

static cmd(*, restarts: int | None = None, hops: int | None = None, seed: int | None = None, threads: int | None = None, mspf: bool = True, resub_shared: bool = True, reset_hops_on_improvement: bool = True, drf_hop: bool = False, drf_iterate: bool = False, truth_tables: bool = False, start_from_smallest: bool = False, start_from_given: bool = False) → aigverse.abc._runner.Command[source]¶

Builds ABC’s &transtoch command without running it.

Parameters:

restarts – Number of restarts (ABC’s -N), or None for ABC’s default. Each restart costs a full transduction run.
hops – Perturbation steps between restarts (ABC’s -M), or None for ABC’s default of 10.
seed – Random seed (ABC’s -R), or None for ABC’s default.
threads – Worker threads (ABC’s -P, at least 1), or None for ABC’s default of 1.
mspf – If True (ABC’s default here), use maximum sets of permissible functions rather than compatible ones.
resub_shared – If True (ABC’s default here), use the ResubShared transduction variant.
reset_hops_on_improvement – If True (ABC’s default here), reset the hop counter whenever a new minimum is found, so a productive direction is followed further.
drf_hop – If True, perturb with drf -z instead of if; mfs2; strash.
drf_iterate – If True, iterate with drf -z instead of &dc2.
truth_tables – If True, reason with truth tables instead of BDDs.
start_from_smallest – If True, restart from the smallest network found so far rather than from the last one.
start_from_given – If True, restart from the network as given rather than from an intermediate result.

Returns:

The command, ready for run_script or run_many.

Raises:

ValueError – If an option is outside the range ABC accepts.

__call__(ntk: aigverse.abc._runner.AigT, *, restarts: int | None = None, hops: int | None = None, seed: int | None = None, threads: int | None = None, mspf: bool = True, resub_shared: bool = True, reset_hops_on_improvement: bool = True, drf_hop: bool = False, drf_iterate: bool = False, truth_tables: bool = False, start_from_smallest: bool = False, start_from_given: bool = False, timeout: float | None = None, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs ABC’s &transtoch command on a network.

Stochastic transduction: it runs transduction repeatedly with randomized parameters and keeps the best result. The most expensive command in this module by a wide margin, and only practical on genuinely small designs. Always pass a timeout.

ABC offers no internal budget for this command either, so timeout kills the process and yields nothing. Bound the work with restarts as well.

Contributed to ABC by Yukio Miyasaka.

Parameters:

ntk – The network to optimize.
restarts – Number of restarts (ABC’s -N), or None for ABC’s default. Each restart costs a full transduction run.
hops – Perturbation steps between restarts (ABC’s -M), or None for ABC’s default of 10.
seed – Random seed (ABC’s -R), or None for ABC’s default.
threads – Worker threads (ABC’s -P, at least 1), or None for ABC’s default of 1.
mspf – If True (ABC’s default here), use maximum sets of permissible functions rather than compatible ones.
resub_shared – If True (ABC’s default here), use the ResubShared transduction variant.
reset_hops_on_improvement – If True (ABC’s default here), reset the hop counter whenever a new minimum is found, so a productive direction is followed further.
drf_hop – If True, perturb with drf -z instead of if; mfs2; strash.
drf_iterate – If True, iterate with drf -z instead of &dc2.
truth_tables – If True, reason with truth tables instead of BDDs.
start_from_smallest – If True, restart from the smallest network found so far rather than from the last one.
start_from_given – If True, restart from the network as given rather than from an intermediate result.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

ValueError – If an option is outside the range ABC accepts.

transtoch: Final[Transtoch]¶: Runs ABC’s &transtoch command on a network, or builds it as a command; see Transtoch.

cec(ntk: Aig, other: Aig, *, conflict_limit: int | None = None, timeout: float | None = None, binary: str | PathLike[str] | None = None) → CecStatus[source]¶

Checks two networks for combinational equivalence with ABC’s &cec.

Unlike everything else in this module this returns a verdict rather than a network. It is an independent second opinion on equivalence_checking(), which is useful precisely because it is a different implementation – if the two ever disagree, one of them has a bug worth finding.

&cec is incomplete under a resource limit, so there are four outcomes and not two. “Not proven equal” and “proven different” are very different answers, which is why this returns a CecStatus rather than a bool and why that enum refuses to be truth-tested.

timeout is handed to ABC as its own limit, so an exhausted budget comes back as CecStatus.TIMEOUT rather than as an exception.

Parameters:

ntk – The first network.
other – The second network. It must have the same numbers of inputs and outputs; &cec matches them by position, not by name.
conflict_limit – Maximum SAT conflicts per node (ABC’s -C, at least 0), or None for ABC’s default of 1000. &cec’s remaining switches select solvers and miter encodings rather than changing the verdict, and are reachable through run_commands().
timeout – Seconds ABC may spend (ABC’s -T), or None for no limit.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The outcome of the check.

Raises:

TypeError – If either argument is not an Aig.
ValueError – If an option is outside the range ABC accepts, or if either argument has a register whose reset value is undefined.
AbcNotFoundError – If no ABC executable could be located.
AbcExecutionError – If ABC failed outright.

stats(ntk: Aig, *, timeout: float | None = None, binary: str | PathLike[str] | None = None) → aigverse.abc._stats.AbcStats[source]¶

Reports ABC’s &ps for a network.

The GIA store’s own view. It agrees with stats() on the counts and adds an average level and a memory figure.

Warning

ABC structurally hashes a network as it reads it, so these counts describe the network ABC ended up with, which can be smaller than the one that was handed over. See stats() for the details.

Parameters:

ntk – The network to measure.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
binary – Overrides the resolved ABC executable for this call only.

Returns:

What ABC reports about the network.

Raises:

TypeError – If ntk is not an Aig.
ValueError – If ntk has a register whose reset value is undefined.
AbcNotFoundError – If no ABC executable could be located.
AbcTimeoutError – If ABC did not terminate within timeout seconds.
AbcExecutionError – If ABC reported an error or printed nothing usable.

run_script(ntk: aigverse.abc._runner.AigT, commands: str | aigverse.abc._runner.Command | Sequence[str | aigverse.abc._runner.Command], *, timeout: float | None = None, use_init_file: bool = False, verbose: bool = False, binary: str | PathLike[str] | None = None) → aigverse.abc._runner.AigT[source]¶

Runs arbitrary &-space commands on a network.

The GIA counterpart of run_script(): the network is transferred with &read/&write so that &-prefixed commands operate on it directly. Equivalent to calling that function with gia=True.

Parameters:

ntk – The network to optimize.
commands – A single ;-separated ABC command string, a Command, or a sequence of individual commands.
timeout – Seconds to wait for ABC to terminate, or None for no limit.
use_init_file – If False (default), ABC is invoked with -s so that no abc.rc is read.
verbose – If True, print everything ABC wrote.
binary – Overrides the resolved ABC executable for this call only.

Returns:

The optimized network, of the same type as ntk.

Raises:

TypeError – If ntk is not an Aig.
ValueError – If no command was given, or if ntk has a register whose reset value is undefined.
AbcNotFoundError – If no ABC executable could be located.
AbcTimeoutError – If ABC did not terminate within timeout seconds.
AbcExecutionError – If ABC reported an error or produced no usable output.

run_many(networks: Iterable[aigverse.abc._runner.AigT], commands: str | aigverse.abc._runner.Command | Sequence[str | aigverse.abc._runner.Command], *, jobs: int | None = ..., timeout: float | None = ..., use_init_file: bool = ..., binary: str | PathLike[str] | None = ..., return_exceptions: Literal[False] = False) → list[aigverse.abc._runner.AigT][source]¶

Runs arbitrary &-space commands over many networks, in parallel.

The GIA counterpart of run_many(): every network is transferred with &read/&write so that &-prefixed commands operate on it directly. Equivalent to calling that function with gia=True.

Parameters:

networks – The networks to optimize. Consumed in full before any work starts.
commands – A single ;-separated ABC command string, a Command, or a sequence of individual commands. The same script runs on every network.
jobs – How many ABC processes to keep running at once. None (default) uses the number of CPUs available to this process, capped at the number of networks; 1 runs inline without a thread pool.
timeout – Seconds to wait for ABC to terminate, per network rather than for the batch as a whole, or None for no limit.
use_init_file – If False (default), ABC is invoked with -s so that no abc.rc is read.
binary – Overrides the resolved ABC executable for this call only. It is resolved once for the whole batch.
return_exceptions – If True, each failing network yields its AbcError in place of a result instead of aborting the batch.

Returns:

The optimized networks, in input order, each of the same type as its input – with AbcError instances in place of the failures when return_exceptions is set.

Raises:

TypeError – If any element of networks is not an Aig.
ValueError – If jobs is below 1, if no command was given, or if a network has a register whose reset value is undefined.
AbcNotFoundError – If no ABC executable could be located.
AbcTimeoutError – If ABC did not terminate within timeout seconds for some network and return_exceptions is not set.
AbcExecutionError – If ABC reported an error for some network and return_exceptions is not set.