Algorithms

This section covers the various algorithms available in aigverse for working with And-Inverter Graphs (AIGs) and other logic representations. These algorithms enable simulation, optimization, and verification of logic networks.

Simulation

Simulation algorithms allow you to evaluate the outputs of a logic network for all possible input combinations, effectively generating truth tables for the network’s outputs and internal nodes.

Functional Simulation

For simulating AIGs with truth tables, the simulate() and simulate_nodes() functions allow you to obtain truth tables for outputs and internal nodes of an AIG.

from aigverse.networks import Aig
from aigverse.algorithms import simulate, simulate_nodes

# Create a sample AIG
aig = Aig()
a = aig.create_pi()
b = aig.create_pi()
f_and = aig.create_and(a, b)
f_or = aig.create_or(a, b)
aig.create_po(f_and)
aig.create_po(f_or)

# Simulate the outputs
output_tts = simulate(aig)

# Print the truth tables
print("Truth tables of outputs:")
for i, tt in enumerate(output_tts):
    print(f"  Output {i}: {tt.to_binary()}")

# Simulate all nodes
node_tts = simulate_nodes(aig)

# Print the truth table of each node
print("\nTruth tables of nodes:")
for node, tt in node_tts.items():
    print(f"  Node {node}: {tt.to_binary()}")

Truth tables of outputs:
  Output 0: 1000
  Output 1: 1110

Truth tables of nodes:
  Node 4: 0001
  Node 3: 1000
  Node 2: 1100
  Node 1: 1010
  Node 0: 0000

Sequential Simulation

simulate() evaluates the combinational logic exactly once and has no notion of a register. Handed a SequentialAig it never assigns the register outputs at all, so every value downstream of one is meaningless.

simulate_sequential() runs the network over a number of clock cycles instead. 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.

A design with no primary inputs runs off its reset state alone. A 4-bit linear-feedback shift register seeded with 0b0001 walks through all fifteen of its non-zero states before repeating:

from aigverse.algorithms import simulate_sequential
from aigverse.networks import AigRegister, SequentialAig

lfsr = SequentialAig()

state = [lfsr.create_ro() for _ in range(4)]
feedback = lfsr.create_xor(state[3], state[2])

# Primary outputs go in before register inputs: both are combinational outputs of
# the same network, and `po_at` / `ri_at` slice that one list by position.
lfsr.create_po(state[3])

lfsr.create_ri(feedback)
for bit in range(3):
    lfsr.create_ri(state[bit])

# Seed the register chain with 0b0001
for bit in range(4):
    register = AigRegister()
    register.init = 1 if bit == 0 else 0
    lfsr.set_register(bit, register)

result = simulate_sequential(lfsr, 15)

print("output: ", "".join(str(int(cycle[0])) for cycle in result.outputs))
print("cycles: ", result.num_cycles)
print("reset:  ", result.reset_state)
print("final:  ", result.final_state)

output:  000100110101111
cycles:  15
reset:   [True, False, False, False]
final:   [True, False, False, False]

A full period brings the registers back to their seed, so final_state matches reset_state.

The result carries two traces, both 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. The state trace is one entry longer than the output trace, because simulating n cycles crosses n + 1 state boundaries:

for cycle, registers in enumerate(result.states):
    print(f"  boundary {cycle:2d}: {''.join(str(int(bit)) for bit in registers)}")

  boundary  0: 1000
  boundary  1: 0100
  boundary  2: 0010
  boundary  3: 1001
  boundary  4: 1100
  boundary  5: 0110
  boundary  6: 1011
  boundary  7: 0101
  boundary  8: 1010
  boundary  9: 1101
  boundary 10: 1110
  boundary 11: 1111
  boundary 12: 0111
  boundary 13: 0011
  boundary 14: 0001
  boundary 15: 1000

Designs with primary inputs are driven by a stimulus, one assignment per cycle. Cycles past the end of it repeat the last assignment, so a single assignment holds for the whole run:

# A three-stage shift register: what goes in comes out three cycles later
shift = SequentialAig()

data = shift.create_pi()
stages = [shift.create_ro() for _ in range(3)]

shift.create_po(stages[2])

shift.create_ri(data)
shift.create_ri(stages[0])
shift.create_ri(stages[1])

for stage in range(3):
    register = AigRegister()
    register.init = 0
    shift.set_register(stage, register)

# A single pulse on the input, then silence
pulse = simulate_sequential(shift, 6, [[True], [False]])

print("output:", "".join(str(int(cycle[0])) for cycle in pulse.outputs))

output: 000100

A register may declare no reset value at all, which is what a fresh AigRegister carries and what an AIGER latch with a nondeterministic reset reads back as. Simulation needs a concrete value, so undefined_reset_value says which one it should use.

Optimization

AIG optimization aims to reduce the number of AND gates and inverters in a circuit while maintaining its logical functionality. Different optimization techniques target various aspects of the AIG structure.

Basic Optimization Workflow

The typical optimization workflow involves:

1. Creating or loading an AIG

2. Applying one or more optimization algorithms

3. Verifying correctness through equivalence checking

from aigverse.io import read_aiger_into_aig

# Load the i10 benchmark circuit - a real-world example
aig = read_aiger_into_aig("examples/i10.aig")

# Print statistics about the loaded circuit
print(f"i10 benchmark:")
print(f"  I/O: {aig.num_pis}/{aig.num_pos}")
print(f"  AND gates: {aig.num_gates}")

i10 benchmark:
  I/O: 257/224
  AND gates: 2675

Resubstitution

Resubstitution identifies portions of logic that can be expressed using existing signals in the network. This technique is particularly effective at identifying and eliminating redundant logic.

from aigverse.algorithms import aig_resubstitution

# Clone the AIG for comparison
aig_resub = aig.clone()

# Apply resubstitution
aig_resub = aig_resubstitution(aig_resub, window_size=12)

print(f"Original AND gates: {aig.num_gates}")
print(f"After resubstitution: {aig_resub.num_gates} AND gates")
print(f"Reduction: {aig.num_gates - aig_resub.num_gates} gates ({(aig.num_gates - aig_resub.num_gates) / aig.num_gates * 100:.2f}%)")

Original AND gates: 2675
After resubstitution: 2173 AND gates
Reduction: 502 gates (18.77%)

Sum-of-Products Refactoring

SOP (Sum of Products) refactoring collapses parts of the AIG into truth tables, then re-synthesizes those portions using Sum-of-Products representations. This can find more efficient implementations for complex logic functions.

from aigverse.algorithms import sop_refactoring

# Clone the AIG for comparison
aig_refactor = aig.clone()

# Apply SOP refactoring
aig_refactor = sop_refactoring(aig_refactor, use_reconvergence_cut=True)

print(f"Original AND gates: {aig.num_gates}")
print(f"After SOP refactoring: {aig_refactor.num_gates} AND gates")
print(f"Reduction: {aig.num_gates - aig_refactor.num_gates} gates ({(aig.num_gates - aig_refactor.num_gates) / aig.num_gates * 100:.2f}%)")

Original AND gates: 2675
After SOP refactoring: 2239 AND gates
Reduction: 436 gates (16.30%)

Cut Rewriting

Cut rewriting identifies small subgraphs (cuts) in the AIG and replaces them with pre-computed optimal implementations from a library. This technique leverages NPN-equivalence classes to find the best possible implementation for each cut.

from aigverse.algorithms import aig_cut_rewriting

# Clone the AIG for comparison
aig_rewrite = aig.clone()

# Apply cut rewriting
aig_rewrite = aig_cut_rewriting(aig_rewrite, cut_size=4)

print(f"Original AND gates: {aig.num_gates}")
print(f"After cut rewriting: {aig_rewrite.num_gates} AND gates")
print(f"Reduction: {aig.num_gates - aig_rewrite.num_gates} gates ({(aig.num_gates - aig_rewrite.num_gates) / aig.num_gates * 100:.2f}%)")

Original AND gates: 2675
After cut rewriting: 2200 AND gates
Reduction: 475 gates (17.76%)

Balancing

Balancing performs (E)SOP factoring to minimize the number of levels in the AIG.

from aigverse.algorithms import balancing
from aigverse.networks import DepthAig

# Clone the AIG for comparison
aig_balance = aig.clone()

# Apply balancing
aig_balance = balancing(aig_balance, rebalance_function="sop")

# Compute depth
original_depth = DepthAig(aig).num_levels
balanced_depth = DepthAig(aig_balance).num_levels

print(f"Original depth: {original_depth} levels")
print(f"After balancing: {balanced_depth} levels")
print(f"Reduction in depth: {original_depth - balanced_depth} levels ({(original_depth - balanced_depth) / original_depth * 100:.2f}%)")

Original depth: 50 levels
After balancing: 32 levels
Reduction in depth: 18 levels (36.00%)

Combining Optimization Techniques

For best results, optimization techniques are typically applied in combination, often in multiple passes. The order of application can significantly impact the final result.

# Apply optimization techniques in sequence
aig_opt = aig.clone()

# First pass
aig_opt = aig_resubstitution(aig_opt)
aig_opt = sop_refactoring(aig_opt)
aig_opt = aig_cut_rewriting(aig_opt)

# Second pass
aig_opt = aig_resubstitution(aig_opt)
aig_opt = sop_refactoring(aig_opt)

print(f"\nTotal optimization results:")
print(f"- Original: {aig.num_gates} AND gates")
print(f"- Optimized: {aig_opt.num_gates} AND gates")
print(f"- Total reduction: {aig.num_gates - aig_opt.num_gates} gates ({(aig.num_gates - aig_opt.num_gates) / aig.num_gates * 100:.2f}%)")

Total optimization results:
- Original: 2675 AND gates
- Optimized: 1950 AND gates
- Total reduction: 725 gates (27.10%)

Some algorithms offer the inplace=True keyword argument for performance-sensitive pipelines of chained optimization. Calling functions such as aig_resubstitution() and sop_refactoring() with inplace=True mutates the passed network and returns None:

from aigverse.algorithms import cleanup_dangling

aig_fast = aig.clone()
aig_resubstitution(aig_fast, inplace=True)
sop_refactoring(aig_fast, inplace=True)

# Explicit cleanup step after in-place chaining
aig_fast = cleanup_dangling(aig_fast)

Note

When choosing this route, users are responsible to call cleanup_dangling() to obtain a structurally valid AIG.

Equivalence Checking

Equivalence checking algorithms verify that two logic networks implement the same function, which is especially important after performing optimizations.

from aigverse.algorithms import equivalence_checking

# Verify that our optimized circuit from the previous section maintains functional equivalence
are_equivalent = equivalence_checking(aig, aig_opt)
print(f"\nOriginal and optimized benchmark circuits are equivalent: {are_equivalent}")
print(f"This confirms our optimization preserved the circuit's functionality while reducing")
print(f"the gate count from {aig.num_gates} to {aig_opt.num_gates} AND gates.")

Original and optimized benchmark circuits are equivalent: True
This confirms our optimization preserved the circuit's functionality while reducing
the gate count from 2086 to 1950 AND gates.