# aigverse.algorithms

Provides synthesis and optimization algorithms for logic network types.

## Module Contents

### equivalence_checking(spec: [Aig](../networks/index.html.md#aigverse.networks.Aig), impl: [Aig](../networks/index.html.md#aigverse.networks.Aig), , conflict_limit: [int](https://docs.python.org/3/builtins/functions.html#int) = 0, functional_reduction: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [bool](https://docs.python.org/3/builtins/functions.html#bool) | [None](https://docs.python.org/3/builtins/constants.html#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**](https://docs.python.org/3/builtins/exceptions.html#RuntimeError) – If miter construction fails due to incompatible interfaces (PI/PO count mismatch).

### cleanup_dangling(ntk: [Aig](../networks/index.html.md#aigverse.networks.Aig), , remove_dangling_pis: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, remove_redundant_pos: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [Aig](../networks/index.html.md#aigverse.networks.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](../networks/index.html.md#aigverse.networks.Aig), , max_pis: [int](https://docs.python.org/3/builtins/functions.html#int) = 6, allow_zero_gain: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, use_reconvergence_cut: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, use_dont_cares: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, use_quick_factoring: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, try_both_polarities: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, consider_inverter_cost: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, inplace: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [Aig](../networks/index.html.md#aigverse.networks.Aig) | [None](https://docs.python.org/3/builtins/constants.html#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**](https://docs.python.org/3/builtins/exceptions.html#RuntimeError) – If refactoring fails in the underlying synthesis engine.

### aig_resubstitution(ntk: [Aig](../networks/index.html.md#aigverse.networks.Aig), , max_pis: [int](https://docs.python.org/3/builtins/functions.html#int) = 8, max_divisors: [int](https://docs.python.org/3/builtins/functions.html#int) = 150, max_inserts: [int](https://docs.python.org/3/builtins/functions.html#int) = 2, skip_fanout_limit_for_roots: [int](https://docs.python.org/3/builtins/functions.html#int) = 1000, skip_fanout_limit_for_divisors: [int](https://docs.python.org/3/builtins/functions.html#int) = 100, verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, use_dont_cares: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, window_size: [int](https://docs.python.org/3/builtins/functions.html#int) = 12, preserve_depth: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, inplace: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [Aig](../networks/index.html.md#aigverse.networks.Aig) | [None](https://docs.python.org/3/builtins/constants.html#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](../networks/index.html.md#aigverse.networks.Aig), , cut_size: [int](https://docs.python.org/3/builtins/functions.html#int) = 4, cut_limit: [int](https://docs.python.org/3/builtins/functions.html#int) = 8, minimize_truth_table: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, allow_zero_gain: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, use_dont_cares: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, min_cand_cut_size: [int](https://docs.python.org/3/builtins/functions.html#int) = 3, min_cand_cut_size_override: [int](https://docs.python.org/3/builtins/functions.html#int) | [None](https://docs.python.org/3/builtins/constants.html#None) = None, preserve_depth: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, very_verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [Aig](../networks/index.html.md#aigverse.networks.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](../networks/index.html.md#aigverse.networks.Aig), , cut_size: [int](https://docs.python.org/3/builtins/functions.html#int) = 4, cut_limit: [int](https://docs.python.org/3/builtins/functions.html#int) = 8, minimize_truth_table: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, only_on_critical_path: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False, rebalance_function: Literal['sop', 'esop'] = 'sop', sop_both_phases: [bool](https://docs.python.org/3/builtins/functions.html#bool) = True, verbose: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [Aig](../networks/index.html.md#aigverse.networks.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**](https://docs.python.org/3/builtins/exceptions.html#ValueError) – If `rebalance_function` is not one of the supported values.

### simulate(ntk: [Aig](../networks/index.html.md#aigverse.networks.Aig)) → [list](https://docs.python.org/3/builtins/stdtypes.html#list)[[TruthTable](../utils/index.html.md#aigverse.utils.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**](https://docs.python.org/3/builtins/exceptions.html#MemoryError) – If the truth tables cannot be allocated due to memory limits.

### simulate_nodes(ntk: [Aig](../networks/index.html.md#aigverse.networks.Aig)) → [dict](https://docs.python.org/3/builtins/stdtypes.html#dict)[[int](https://docs.python.org/3/builtins/functions.html#int), [TruthTable](../utils/index.html.md#aigverse.utils.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**](https://docs.python.org/3/builtins/exceptions.html#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](https://docs.python.org/3/builtins/stdtypes.html#list)[[list](https://docs.python.org/3/builtins/stdtypes.html#list)[[bool](https://docs.python.org/3/builtins/functions.html#bool)]]*

Primary output values, one list per clock cycle.

#### *property* states *: [list](https://docs.python.org/3/builtins/stdtypes.html#list)[[list](https://docs.python.org/3/builtins/stdtypes.html#list)[[bool](https://docs.python.org/3/builtins/functions.html#bool)]]*

Register values, one list per state boundary.

#### *property* num_cycles *: [int](https://docs.python.org/3/builtins/functions.html#int)*

Number of clock cycles simulated.

#### *property* reset_state *: [list](https://docs.python.org/3/builtins/stdtypes.html#list)[[bool](https://docs.python.org/3/builtins/functions.html#bool)]*

The state the registers were reset to.

#### *property* final_state *: [list](https://docs.python.org/3/builtins/stdtypes.html#list)[[bool](https://docs.python.org/3/builtins/functions.html#bool)]*

The state the registers held after the last cycle.

#### \_\_len_\_() → [int](https://docs.python.org/3/builtins/functions.html#int)

### simulate_sequential(ntk: [SequentialAig](../networks/index.html.md#aigverse.networks.SequentialAig), num_cycles: [int](https://docs.python.org/3/builtins/functions.html#int), stimulus: [Sequence](https://docs.python.org/3/library/collections.abc.html#collections.abc.Sequence)[[Sequence](https://docs.python.org/3/library/collections.abc.html#collections.abc.Sequence)[[bool](https://docs.python.org/3/builtins/functions.html#bool)]] = [], undefined_reset_value: [bool](https://docs.python.org/3/builtins/functions.html#bool) = False) → [SequentialSimulationResult](#aigverse.algorithms.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()`](#aigverse.algorithms.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**](https://docs.python.org/3/builtins/exceptions.html#ValueError) – If an assignment in `stimulus` does not have one value per primary input.