aigverse.algorithms

Provides synthesis and optimization algorithms for logic network types.

Module Contents

equivalence_checking(spec: Aig, impl: Aig, *, conflict_limit: int = 0, functional_reduction: bool = True, verbose: bool = False) → bool | None

Checks functional equivalence between a specification and implementation network using SAT solving.

Parameters:

  • spec – The specification network.

  • impl – The implementation network.

  • conflict_limit – SAT conflict limit. A value of 0 means no limit.

  • functional_reduction – Whether to perform functional reduction of the miter before checking.

  • verbose – Whether to print verbose progress output.

Returns:

True if equivalent, False if not equivalent, or None if the procedure did not finish before the configured limit.

Raises:

RuntimeError – If miter construction fails due to incompatible interfaces (PI/PO count mismatch).

cleanup_dangling(ntk: Aig, *, remove_dangling_pis: bool = False, remove_redundant_pos: bool = False) → Aig

Removes dangling logic (dead nodes) from a network.

Parameters:

  • ntk – The input logic network.

  • remove_dangling_pis – Whether to also remove dangling primary inputs.

  • remove_redundant_pos – Whether to remove redundant primary outputs.

Returns:

A cleaned network with dangling structures removed.

sop_refactoring(ntk: Aig, *, max_pis: int = 6, allow_zero_gain: bool = False, use_reconvergence_cut: bool = False, use_dont_cares: bool = False, use_quick_factoring: bool = True, try_both_polarities: bool = True, consider_inverter_cost: bool = False, verbose: bool = False, inplace: bool = False) → Aig | None

Performs SOP-based network refactoring.

Parameters:

  • ntk – The input logic network.

  • max_pis – Maximum number of leaves used in local windows.

  • allow_zero_gain – Whether substitutions with zero gain are allowed.

  • use_reconvergence_cut – Whether to use reconvergence-driven cuts.

  • use_dont_cares – Whether to use don’t-care information.

  • use_quick_factoring – Whether to use the quick SOP factoring heuristic.

  • try_both_polarities – Whether both output polarities are explored.

  • consider_inverter_cost – Whether inverter cost is included in optimization.

  • verbose – Whether to print verbose progress output.

  • inplace – Whether to mutate ntk in place. A network being transformed in place must not be shared with another thread.

Returns:

The refactored network if inplace is False. Otherwise None.

Raises:

RuntimeError – If refactoring fails in the underlying synthesis engine.

aig_resubstitution(ntk: Aig, *, max_pis: int = 8, max_divisors: int = 150, max_inserts: int = 2, skip_fanout_limit_for_roots: int = 1000, skip_fanout_limit_for_divisors: int = 100, verbose: bool = False, use_dont_cares: bool = False, window_size: int = 12, preserve_depth: bool = False, inplace: bool = False) → Aig | None

Performs AIG resubstitution-based optimization.

Parameters:

  • ntk – The input logic network.

  • max_pis – Maximum number of leaves in a local window.

  • max_divisors – Maximum number of candidate divisors.

  • max_inserts – Maximum number of inserted nodes per replacement.

  • skip_fanout_limit_for_roots – Fanout threshold to skip root candidates.

  • skip_fanout_limit_for_divisors – Fanout threshold to skip divisor candidates.

  • verbose – Whether to print verbose progress output.

  • use_dont_cares – Whether to use don’t-care information.

  • window_size – Window size used for don’t-care computation.

  • preserve_depth – Whether replacements must preserve depth.

  • inplace – Whether to mutate ntk in place. A network being transformed in place must not be shared with another thread.

Returns:

The optimized network if inplace is False. Otherwise None.

aig_cut_rewriting(ntk: Aig, *, cut_size: int = 4, cut_limit: int = 8, minimize_truth_table: bool = True, allow_zero_gain: bool = False, use_dont_cares: bool = False, min_cand_cut_size: int = 3, min_cand_cut_size_override: int | None = None, preserve_depth: bool = False, verbose: bool = False, very_verbose: bool = False) → Aig

Rewrites an AIG network using cut-based NPN resynthesis.

Parameters:

  • ntk – The input logic network.

  • cut_size – Maximum cut size used during cut enumeration.

  • cut_limit – Maximum number of cuts retained per node.

  • minimize_truth_table – Whether to minimize cut truth tables.

  • allow_zero_gain – Whether replacements with zero gain are allowed.

  • use_dont_cares – Whether to use don’t-care information.

  • min_cand_cut_size – Minimum candidate cut size.

  • min_cand_cut_size_override – Optional override for minimum candidate cut size.

  • preserve_depth – Whether replacements must preserve network depth.

  • verbose – Whether to print verbose progress output.

  • very_verbose – Whether to print highly detailed progress output.

Returns:

A rewritten network.

balancing(ntk: Aig, *, cut_size: int = 4, cut_limit: int = 8, minimize_truth_table: bool = True, only_on_critical_path: bool = False, rebalance_function: Literal['sop', 'esop'] = 'sop', sop_both_phases: bool = True, verbose: bool = False) → Aig

Balances a network using SOP or ESOP-based local restructuring.

Parameters:

  • ntk – The input logic network.

  • cut_size – Maximum cut size used during cut enumeration.

  • cut_limit – Maximum number of cuts retained per node.

  • minimize_truth_table – Whether to minimize cut truth tables during enumeration.

  • only_on_critical_path – Whether to balance only nodes on the critical path.

  • rebalance_function – Rebalancing engine to use. Supported values are "sop" and "esop".

  • sop_both_phases – Whether to consider both phases in SOP/ESOP balancing.

  • verbose – Whether to print verbose progress output.

Returns:

A new balanced network.

Raises:

ValueError – If rebalance_function is not one of the supported values.

simulate(ntk: Aig) → list[TruthTable]

Simulates all primary outputs of a network as truth tables.

Parameters:

ntk – The input logic network.

Returns:

A list containing one truth table per primary output.

Raises:

MemoryError – If the truth tables cannot be allocated due to memory limits.

simulate_nodes(ntk: Aig) → dict[int, TruthTable]

Simulates all nodes of a network as truth tables.

Parameters:

ntk – The input logic network.

Returns:

A dictionary that maps node identifiers to truth tables.

Raises:

MemoryError – If the truth tables cannot be allocated due to memory limits.

class SequentialSimulationResult

Represents the outcome of simulating a sequential network over several clock cycles.

Both traces are indexed by clock cycle first: outputs[cycle][index] is the value primary output index took in that cycle, and states[cycle][index] the value register index held while that cycle was evaluated.

states is one entry longer than outputs, because simulating n cycles crosses n + 1 state boundaries. The first is the reset state the run started from and the last is the state it ended in.

property outputs: list[list[bool]]

Primary output values, one list per clock cycle.

property states: list[list[bool]]

Register values, one list per state boundary.

property num_cycles: int

Number of clock cycles simulated.

property reset_state: list[bool]

The state the registers were reset to.

property final_state: list[bool]

The state the registers held after the last cycle.

__len__() → int
simulate_sequential(ntk: SequentialAig, num_cycles: int, stimulus: Sequence[Sequence[bool]] = [], undefined_reset_value: bool = False) → SequentialSimulationResult

Simulates a sequential network over a number of clock cycles.

Every register starts at its reset value, the combinational logic is evaluated once per cycle, the primary outputs are recorded, and the register inputs are latched into the register outputs for the next cycle.

This is what distinguishes it from simulate(), which evaluates the combinational logic exactly once and has no notion of a register.

Parameters:

  • ntk – The sequential network to simulate.

  • num_cycles – Number of clock cycles to run.

  • stimulus – Primary input assignments, one list of ntk.num_pis values per clock cycle. Cycles past the end of the stimulus repeat its last assignment, so a single assignment holds for the whole run. Defaults to holding every primary input at False, which is all a design without primary inputs needs.

  • undefined_reset_value – Value a register starts at when its reset value is undefined, which is what a register defaults to and what an AIGER latch with a nondeterministic reset reads back as.

Returns:

The primary output values and the register values, per clock cycle.

Raises:

ValueError – If an assignment in stimulus does not have one value per primary input.