aigverse 0.0.7

A Python library for working with logic networks, synthesis, and optimization.

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

[!Important] This project is still in the early stages of development. The API is subject to change, and some features may not be fully implemented. I appreciate your patience and understanding as work to improve the library continues.

aigverse is a Python framework designed to bridge the gap between logic synthesis and AI/ML applications. It allows you to represent and manipulate logic circuits efficiently, making it easier to integrate logic synthesis tasks into machine learning pipelines. By leveraging the powerful EPFL Logic Synthesis Libraries, particularly mockturtle, aigverse provides a high-level Python interface to state-of-the-art algorithms for And-Inverter Graph (AIG) manipulation and logic synthesis, widely used in formal verification, hardware design, and optimization tasks.

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.
• Integration with Machine Learning: Convenient integration with popular data science libraries.

Motivation

As AI and machine learning (ML) increasingly impact hardware design automation, there's a growing need for tools that integrate logic synthesis with ML workflows. aigverse provides a Python-friendly interface for logic synthesis, making it easier to develop applications that blend both AI/ML and traditional circuit synthesis techniques. With aigverse, you can parse, manipulate, and optimize logic circuits directly from Python. Eventually, we aim to provide seamless integration with popular ML libraries, enabling the development of novel AI-driven synthesis and optimization tools.

Installation

aigverse requires Python 3.8+ and is built using the EPFL Logic Synthesis Libraries with pybind11. To install aigverse:

pip install aigverse

Usage

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 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()}")

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
for fanin in aig.fanins(f_and):
    print(f"Fanin of {f_and}: {fanin}")

Logic Optimization

You can optimize AIGs using various algorithms. For example, you can perform resubstitution to simplify logic using shared divisors.

from aigverse import aig_resubstitution

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

# Optimize the AIG using resubstitution
aig_resubstitution(aig)

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

Equivalence Checking

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

from aigverse import equivalence_checking

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

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

AIGER Files

You can read and write (ASCII) AIGER files.

Parsing

from aigverse import read_aiger_into_aig, read_ascii_aiger_into_aig

# Read AIGER files into AIG networks
aig1 = read_aiger_into_aig("example.aig")
aig2 = read_ascii_aiger_into_aig("example.aag")

# Print the size of the AIGs
print(f"AIG Size: {aig1.size()}")
print(f"AIG Size: {aig2.size()}")

Writing

from aigverse import write_aiger

# Write an AIG network to an AIGER file
write_aiger(aig, "example.aig")

Exporting Edge Lists

You can export the AIG as an edge list, which is useful for integration with graph libraries like NetworkX.

from aigverse import to_edge_list

# Export the AIG as an edge list
edges = to_edge_list(aig)
print(edges)

# Convert to list of tuples
edges = [(e.source, e.target, e.weight) for e in edges]

Contributing

Contributions are welcome! If you'd like to contribute to aigverse, please submit a pull request or open an issue. If appreciate feedback and suggestions for improving the library.

License

aigverse is available under the MIT License.