aigverse: A Python Library for Logic Networks, Synthesis, and Optimization

aigverse is an open-source infrastructure project that brings mature logic synthesis capabilities into Python-first workflows. Rather than reimplementing synthesis algorithms in Python, it wraps high-performance C/C++ backends with an idiomatic Python interface. aigverse is built directly upon the EPFL Logic Synthesis Libraries, particularly mockturtle, kitty, and lorina, providing reusable support for And-Inverter Graph (AIG) construction, manipulation, optimization and equivalence-checking flows, dataset generation, and export to graph and array representations for downstream data science and ML pipelines.

✨ Features

• Efficient Logic Representation: Use And-Inverter Graphs (AIGs) to model and manipulate logic circuits in Python.
• File Format Support: Read and write AIGER, Verilog, Bench, PLA, ... files for interoperability with other logic synthesis tools.
• C++ Backend: Leverage the performance of the EPFL Logic Synthesis Libraries for fast logic synthesis and optimization.
• High-Level API: Simplify logic synthesis tasks with a Pythonic interface for AIG manipulation and optimization.
• ML/Data Science Interoperability: Optional adapters for graph and array representations used in Python data science and machine learning workflows.
• Benchmark Suites: On-demand access to standard benchmark circuits (e.g., the EPFL suite), downloaded once and cached locally.
• ABC Integration: Optionally run ABC optimization scripts such as resyn2 or compress2rs on your networks, driving an ABC executable you already have installed. No ABC is bundled.

🤔 Motivation

Logic synthesis algorithms are predominantly implemented in highly optimized C/C++ toolchains, while modern ML experimentation is often Python-first. Without reusable infrastructure, projects frequently end up reimplementing synthesis functionality in Python or maintaining brittle wrapper and file-conversion pipelines around external tools. aigverse addresses this recurring engineering gap by exposing mature synthesis capabilities through a streamlined Python API. This enables circuit construction and manipulation, optimization and equivalence-checking flows, and export to ML-ready graph or numeric representations in one reusable library. aigverse wraps the EPFL Logic Synthesis Libraries with nanobind to provide a Pythonic interface to high-performance C/C++ synthesis backends.

📦 Installation

aigverse is available via PyPI for all major operating systems, with a single Stable ABI wheel per platform that covers every supported Python from 3.10 up. Free-threaded interpreters are not supported yet, pending the stable ABI that Python 3.15 brings them.

pip install aigverse

🔌 Adapters

To keep the core library lightweight, ML and data science adapters are optional and not installed by default. They provide reusable conversion paths from AIGs to graph and array formats for Python workflows (such as NetworkX and NumPy). To install aigverse with the adapters extra, use:

pip install "aigverse[adapters]"

This will install additional dependencies required for ML workflows. See the documentation for more details.

🚀 Usage

The following demonstrates core workflows in aigverse. Detailed documentation and examples are available at ReadTheDocs.

🏗️ Basic Example: Creating an AIG

In aigverse, you can create a simple And-Inverter Graph (AIG) and manipulate it using various logic operations.

from aigverse.networks import Aig

# Create a new AIG network
aig = Aig()

# Create primary inputs
x1 = aig.create_pi()
x2 = aig.create_pi()

# Create logic gates
f_and = aig.create_and(x1, x2)  # AND gate
f_or = aig.create_or(x1, x2)  # OR gate

# Create primary outputs
aig.create_po(f_and)
aig.create_po(f_or)

# Print the size of the AIG network
print(f"AIG Size: {aig.size}")

Note that all primary inputs (PIs) must be created before any logic gates.

🔍 Iterating over AIG Nodes

You can iterate over all nodes in the AIG, or specific subsets like the primary inputs or only logic nodes (gates).

# Iterate over all nodes in the AIG
for node in aig.nodes():
    print(f"Node: {node}")

# Iterate only over primary inputs
for pi in aig.pis():
    print(f"Primary Input: {pi}")

# Iterate only over logic nodes (gates)
for gate in aig.gates():
    print(f"Gate: {gate}")

# Iterate over the fanins of a node
n_and = aig.get_node(f_and)
for fanin in aig.fanins(n_and):
    print(f"Fanin of {n_and}: {fanin}")

🏷️ Network and Signal Names

Named AIGs allow you to assign human-readable names to the network, inputs, outputs, and internal signals.

from aigverse.networks import NamedAig

# Create a named AIG
named_aig = NamedAig()
named_aig.set_network_name("full_adder")

# Create named primary inputs and logic
a = named_aig.create_pi("a")
b = named_aig.create_pi("b")
cin = named_aig.create_pi("cin")

sum = named_aig.create_xor3(a, b, cin)
carry = named_aig.create_maj(a, b, cin)

# Assign names to signals and create named outputs
named_aig.set_name(sum, "sum")
named_aig.create_po(carry, "carry_output")

# Retrieve names
print(f"Network: {named_aig.get_network_name()}")
print(f"Signal: {named_aig.get_name(sum)}")

Named AIGs are automatically created when reading Verilog or AIGER files with naming information.

📏 Depth and Level Computation

You can compute the depth of the AIG network and the level of each node. Depth information is useful for estimating the critical path delay of a respective circuit.

from aigverse.networks import DepthAig

depth_aig = DepthAig(aig)
print(f"Depth: {depth_aig.num_levels}")
for node in aig.nodes():
    print(f"Level of {node}: {depth_aig.level(node)}")

🕸️ AIGs with Fanout Information

If needed, you can retrieve the fanouts of AIG nodes as well:

from aigverse.networks import FanoutAig

fanout_aig = FanoutAig(aig)
n_and = aig.get_node(f_and)
# Iterate over the fanouts of a node
for fanout in fanout_aig.fanouts(n_and):
    print(f"Fanout of node {n_and}: {fanout}")

🔄 Sequential AIGs

aigverse also supports sequential AIGs, which are AIGs with registers.

from aigverse.networks import SequentialAig

seq_aig = SequentialAig()
x1 = seq_aig.create_pi()  # Regular PI
x2 = seq_aig.create_ro()  # Register output (sequential PI)

f_and = seq_aig.create_and(x1, x2)  # AND gate

seq_aig.create_ri(f_and)  # Register input (sequential PO)

print(seq_aig.registers())  # Prints the association of registers

It is to be noted that the construction of sequential AIGs comes with some caveats:

1. All register outputs (ROs) must be created after all primary inputs (PIs).
2. All register inputs (RIs) must be created after all primary outputs (POs).
3. As for regular AIGs, all PIs and ROs must be created before any logic gates.

⚡ Logic Optimization

You can optimize AIGs using various algorithms. For example, you can perform resubstitution to simplify logic using shared divisors. Similarly, refactoring collapses maximal fanout-free cones (MFFCs) into truth tables and resynthesizes them into new structures. Cut rewriting optimizes the AIG by replacing cuts with improved ones from a pre-computed NPN database. Finally, balancing performs (E)SOP factoring to minimize the number of levels in the AIG.

from aigverse.algorithms import (
    aig_resubstitution,
    sop_refactoring,
    aig_cut_rewriting,
    balancing,
    cleanup_dangling,
)

# Clone the AIG network for size comparison
aig_clone = aig.clone()

# Optimize the AIG with several optimization algorithms.
# By default, each algorithm returns a *new* cleaned AIG.
aig_opt = aig
for optimization in [aig_resubstitution, sop_refactoring, aig_cut_rewriting, balancing]:
    aig_opt = optimization(aig_opt)

# Print the size of the unoptimized and optimized AIGs
print(f"Original AIG Size:  {aig_clone.size}")
print(f"Optimized AIG Size: {aig_opt.size}")

# Some algorithms offer in-place transformations for performance-oriented pipelines
for optimization in [aig_resubstitution, sop_refactoring]:
    optimization(aig, inplace=True)
aig = cleanup_dangling(aig)

🎲 Random AIG Generation

The aigverse.generators module provides reproducible random AIG generation via random_aig.

from aigverse.generators import random_aig

# One random AIG
aig = random_aig(num_pis=4, num_gates=20, seed=123)

# Python-side batch generation
dataset = [random_aig(num_pis=4, num_gates=20, seed=1000 + i) for i in range(16)]

🧱 Structured Generator Networks

The same module also provides high-level arithmetic and control generators that return complete benchmark networks.

from aigverse.generators import binary_decoder, ripple_carry_adder, multiplexer

adder = ripple_carry_adder(8)
mux = multiplexer(8)
decoder = binary_decoder(8)

print(adder.num_pis, adder.num_pos, adder.num_gates)
print(mux.num_pis, mux.num_pos, mux.num_gates)
print(decoder.num_pis, decoder.num_pos, decoder.num_gates)

📊 Benchmark Loading

The aigverse.benchmarks module fetches standard benchmark suites on demand and caches them locally, so a script can name a benchmark instead of carrying a downloader and a checked-in copy of the data. The EPFL combinational suite is supported out of the box.

from aigverse.benchmarks import epfl, epfl_names

# List the benchmark names in a category
print(epfl_names("arithmetic"))  # ('adder', 'bar', 'div', ...)

# Downloads once and caches thereafter, returned as a NamedAig
aig = epfl("ctrl")
print(f"{aig.num_pis} inputs, {aig.num_pos} outputs, {aig.num_gates} AND gates")

For more details, including cache configuration and revision pinning, see the benchmarks documentation.

✅ Equivalence Checking

Equivalence of AIGs (e.g., after optimization) can be checked using SAT-based equivalence checking.

from aigverse.algorithms import equivalence_checking

# Perform equivalence checking
equiv = equivalence_checking(aig1, aig2)

if equiv:
    print("AIGs are equivalent!")
else:
    print("AIGs are NOT equivalent!")

🅰️ ABC Integration

aigverse can hand networks to ABC and read the result back, so ABC's optimization scripts are available as ordinary Python functions. No ABC is bundled: the bridge drives an executable you already have installed, found on PATH as abc, or pointed at with the AIGVERSE_ABC environment variable or abc.set_abc_binary(). Importing the module always succeeds, so use abc.is_available() to check before calling.

from aigverse import abc
from aigverse.algorithms import equivalence_checking
from aigverse.generators import carry_lookahead_adder

aig = carry_lookahead_adder(16)

# Returns a new network; the input is left untouched
optimized = abc.resyn2(aig)

print(f"{aig.num_gates} -> {optimized.num_gates} AND gates")
print(f"Equivalent: {equivalence_checking(aig, optimized)}")

The other named scripts (resyn, resyn3, compress, compress2, resyn2rs, compress2rs, and dc2) work the same way, as do the individual commands abc.balance, abc.rewrite, abc.refactor, and abc.resub. See the ABC documentation for the full set.

📄 File Format Support

You can read and write AIGs in various file formats, including (ASCII) AIGER, gate-level Verilog and PLA.

✏️ Writing

from aigverse.io import write_aiger, write_verilog, write_dot

# Write an AIG network to an AIGER file
write_aiger(aig, "example.aig")
# Write an AIG network to a Verilog file
write_verilog(aig, "example.v")
# Write an AIG network to a DOT file
write_dot(aig, "example.dot")

👓 Parsing

from aigverse.io import (
    read_aiger_into_aig,
    read_ascii_aiger_into_aig,
    read_verilog_into_aig,
    read_pla_into_aig,
)

# Read AIGER files into AIG networks
aig1 = read_aiger_into_aig("example.aig")
aig2 = read_ascii_aiger_into_aig("example.aag")
# Read a Verilog file into an AIG network
aig3 = read_verilog_into_aig("example.v")
# Read a PLA file into an AIG network
aig4 = read_pla_into_aig("example.pla")

Additionally, you can read AIGER files into sequential AIGs using read_aiger_into_sequential_aig and read_ascii_aiger_into_sequential_aig.

🥒 pickle Support

AIGs support Python's pickle protocol, allowing you to serialize and deserialize AIG objects for persistent storage or interface with data science or machine learning workflows.

import pickle

with open("aig.pkl", "wb") as f:
    pickle.dump(aig, f)

with open("aig.pkl", "rb") as f:
    unpickled_aig = pickle.load(f)

You can also pickle multiple AIGs at once by storing them in a tuple or list.

🧠 Machine Learning Integration

With the adapters extra, you can convert an AIG to a NetworkX directed graph, enabling visualization and use with graph-based ML tools:

import aigverse.adapters

G = aig.to_networkx(levels=True, fanouts=True, node_tts=True)

Graph, node, and edge attributes provide logic, level, fanout, and function information for downstream ML or visualization tasks.

For more details and examples, see the machine learning integration documentation.

🔢 Truth Tables

Small Boolean functions can be efficiently represented using truth tables. aigverse enables the creation and manipulation of truth tables by wrapping a portion of the kitty library.

🎉 Creation

from aigverse.utils import TruthTable

# Initialize a truth table with 3 variables
tt = TruthTable(3)
# Create a truth table from a hex string representing the MAJ function
tt.create_from_hex_string("e8")

🔧 Manipulation

# Flip each bit in the truth table
for i in range(tt.num_bits()):
    print(f"Flipping bit {int(tt.get_bit(i))}")
    tt.flip_bit(i)

# Print a binary string representation of the truth table
print(tt.to_binary())

# Clear the truth table
tt.clear()

# Check if the truth table is constant 0
print(tt.is_const0())

🔣 Symbolic Simulation of AIGs

from aigverse.algorithms import simulate, simulate_nodes

# Obtain the truth table of each AIG output
tts = simulate(aig)

# Print the truth tables
for i, tt in enumerate(tts):
    print(f"PO{i}: {tt.to_binary()}")

# Obtain the truth tables of each node in the AIG
n_to_tt = simulate_nodes(aig)

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

📃 Exporting as Lists or NumPy Arrays

For machine learning applications, it is often useful to convert truth tables into standard data structures like Python lists or NumPy arrays. Since TruthTable objects are iterable, conversion is straightforward.

import numpy as np

# Export to a list
tt_list = list(tt)

# Export to NumPy arrays
tt_np_bool = np.array(tt)
tt_np_int = np.array(tt, dtype=np.int32)
tt_np_float = np.array(tt, dtype=np.float64)

🥒 pickle Support

Truth tables also support Python's pickle protocol, allowing you to serialize and deserialize them.

import pickle

with open("tt.pkl", "wb") as f:
    pickle.dump(tt, f)

with open("tt.pkl", "rb") as f:
    unpickled_tt = pickle.load(f)

🎤 Learn More

For a deeper dive into the vision and technical details behind aigverse, check out the presentation from the Free Silicon Conference (FSiC) 2025:

"aigverse: Toward machine learning-driven logic synthesis" 📄 Slides available on the FSiC wiki

This talk presents the same core infrastructure thesis: closing the software gap between high-performance synthesis tooling and Python-first ML workflows.

🙌 Contributing

Contributions are welcome! If you'd like to contribute to aigverse, please see the contribution guide. I appreciate feedback and suggestions for improving the library.

💼 Support and Consulting

aigverse is and will always be a free, open-source library. If you or your organization require dedicated support, specific new features, or integration of aigverse into your projects, professional consulting services are available. This is a great way to get the features you need while also supporting the ongoing maintenance and development of the library.

For inquiries, please reach out to @marcelwa. More information can be found in the documentation.

📜 License

aigverse is available under the MIT License.