Table of Contents
- About PyAiger
- Installation
- Development workflow
- Boolean Expression DSL
- Sequential Circuit DSL
- Extra
- Ecosystem
- Related Projects
- Citing
About PyAiger
- Q: How is Py-Aiger pronounced? A: Like "pie" + "grrr".
- Q: Why python? Aren't you worried about performance?! A: No. The goals of this library are ease of use and hackability.
- Q: No, I'm really concerned about performance! A: This library is not suited to implement logic solvers. For everything else, such as the creation and manipulation of circuits with many thousands of gates in between solver calls, the library is really fast enough.
- Q: Where does the name come from? A: Aiger is a popular circuit format. The format is used in hardware model checking, synthesis, and is supported by ABC. The name is a combination of AIG (standing for And-Inverter-Graph) and the mountain Eiger.
Installation
If you just need to use aiger, you can just run:
$ pip install py-aiger
For developers, see the Development workflow section below.
Development workflow
Development uses uv for reproducible dependency and workspace management.
$ uv install
Commit the resulting uv.lock whenever dependencies change, and use
uv run <command> for recurring tasks such as:
$ uv run pytest
In a Nix shell give uv access to the locked environment via:
nix develop --command bash -c "uv run pytest"
Updating the changelog
Commitizen is bundled in the Nix dev shell so cz bump is available inside the locked environment. Run:
$ cz bump
Usage
Commands shown here assume you're executing Python through uv run (e.g., uv run python or via nix develop --command bash -c "uv run python") so the locked dependencies are used.
import aiger
x, y, z, w = aiger.atoms('x', 'y', 'z', 'w')
expr1 = z.implies(x & y)
expr2 = z & w
circ1 = expr1.with_output('z') \ # Get AIG for expr1 with output 'z'.
.aig
circ2 = circ1 >> circ2 # Feed outputs of circ1 into circ2.
Boolean Expression DSL
While powerful, when writing combinatorial circuits, the Sequential Circuit DSL can be somewhat clumsy. For this common usecase, we have developed the Boolean Expression DSL. All circuits generated this way have a single output.
import aiger
x, y, z = aiger.atoms('x', 'y', 'z')
expr1 = x & y # circuit with inputs 'x', 'y' and 1 output computing x AND y.
expr2 = x | y # logical or.
expr3 = x ^ y # logical xor.
expr4 = x == y # logical ==, xnor.
expr5 = x.implies(y)
expr6 = ~x # logical negation.
expr7 = aiger.ite(x, y, z) # if x then y else z.
# Atoms can be constants.
expr8 = x & True # Equivalent to just x.
expr9 = x & False # Equivalent to const False.
# Specifying output name of boolean expression.
# - Output is a long uuid otherwise.
expr10 = expr5.with_output('x_implies_y')
assert expr10.output == 'x_implies_y'
# And you can inspect the AIG if needed.
circ = x.aig
# And of course, you can get a BoolExpr from a single output aig.
expr10 = aiger.BoolExpr(circ)
Sequential Circuit DSL
import aiger
from aiger import utils
# Parser for ascii AIGER format.
aig1 = aiger.load(path_to_aig1_file.aag)
aig2 = aiger.load(path_to_aig2_file.aag)
Sequential composition
aig3 = aig1 >> aig2
Parallel composition
aig4 = aig1 | aig2
Circuits with Latches and Delayed Feedback
Sometimes one requires some outputs to be feed back into the circuits
as time delayed inputs. This can be accomplished using the loopback
method. This method takes in a variable number of dictionaries
encoding how to wire an input to an output. The wiring dictionaries
with the following keys and default values:
| Key | Default | Meaning |
|---|---|---|
| input | Input port | |
| output | Output port | |
| latch | input | Latch name |
| init | True | Initial latch value |
| keep_output | True | Keep loopbacked output as output |
# Connect output y to input x with delay, initialized to True.
# (Default initialization is False.)
aig5 = aig1.loopback({
"input": "x", "output": "y",
})
aig6 = aig1.loopback({
"input": "x", "output": "y",
}, {
"input": "z", "output": "z", "latch": "z_latch",
"init": False, "keep_outputs": False
})
Relabeling
There are two syntaxes for relabeling. The first uses indexing syntax in a nod to notation often used variable substition in math.
The syntax is the relabel method, which is preferable when one wants
to be explicit, even for those not familar with py-aiger.
# Relabel input 'x' to 'z'.
aig1['i', {'x': 'z'}]
aig1.relabel('input', {'x': 'z'})
# Relabel output 'y' to 'w'.
aig1['o', {'y': 'w'}]
aig1.relabel('output', {'y': 'w'})
# Relabel latches 'l1' to 'l2'.
aig1['l', {'l1': 'l2'}]
aig1.relabel('latch', {'l1': 'l2'})
Evaluation
# Combinatoric evaluation.
aig3(inputs={'x':True, 'y':False})
# Sequential evaluation.
sim = aig3.simulate([{'x': 0, 'y': 0},
{'x': 1, 'y': 2},
{'x': 3, 'y': 4}])
# Simulation Coroutine
sim = aig3.simulator() # Coroutine
next(sim) # Initialize
print(sim.send({'x': 0, 'y': 0}))
print(sim.send({'x': 1, 'y': 2}))
print(sim.send({'x': 3, 'y': 4}))
# Unroll
aig4 = aig3.unroll(steps=10, init=True)
Useful circuits
# Fix input x to be False.
aig4 = aiger.source({'x': False}) >> aig3
# Remove output y.
aig4 = aig3 >> aiger.sink(['y'])
# Create duplicate w of output y.
aig4 = aig3 >> aiger.tee({'y': ['y', 'w']})
Extra
aiger.common.eval_order(aig1) # Returns topological ordering of circuit gates.
# Convert object into an AIG from multiple formats including BoolExpr, AIG, str, and filepaths.
aiger.to_aig(aig1)
Ecosystem
Stable
- py-aiger-bv: Extension of pyAiger for manipulating sequential bitvector circuits.
- py-aiger-cnf: BoolExpr to Object representing CNF. Mostly used for interfacing with py-aiger-sat.
- py-aiger-past-ltl: Converts Past Linear Temporal Logic to aiger circuits.
- py-aiger-coins: Library for creating circuits that encode discrete distributions.
- py-aiger-sat: Bridge between py-aiger and py-sat.
- py-aiger-bdd: Aiger <-> BDD bridge.
- py-aiger-gridworld: Create aiger circuits representing gridworlds.
- py-aiger-dfa: Convert between finite automata and sequential circuits.
Underdevelopment
- py-aiger-spectral: A tool for performing (Fourier) Analysis of Boolean Functions.
- py-aiger-abc: Aiger and abc bridge.
Related Projects
- pyAig: Another python library for working with AIGER circuits.
1 maintainer
Release files for py-aiger 8.1.0
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| py_aiger-8.1.0.tar.gz | 17.2 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| py_aiger-8.1.0-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 37.6 kB
Release files / py_aiger-8.1.0.tar.gz
| Download URL | py_aiger-8.1.0.tar.gz |
|---|---|
| Size | 17.2 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
a1a26bb0e2edba8bb5407d8b33f532f8f1cc1d897148eaf13a65ef70692b6d2d
|
|
BLAKE2b-256 checksum How to use checksums |
a26bb08eb1c8370044a5ff9a7bdc90472580797f4ef7c3180b2f689cdc284f2f
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.9.18 {"installer":{"name":"uv","version":"0.9.18","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"NixOS","version":"25.11","id":"xantusia","libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}
|
Release files / py_aiger-8.1.0-py3-none-any.whl
| Download URL | py_aiger-8.1.0-py3-none-any.whl |
|---|---|
| Size | 20.4 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
485033ad4258a1f1f605b31956d750c8ad99e1dfd4c0d38875fc1a1c139c0d6f
|
|
BLAKE2b-256 checksum How to use checksums |
fe091b9bde7f58093b4836a0b7f7dcacabf7dedba96b14e2997d2cc7124018b3
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.9.18 {"installer":{"name":"uv","version":"0.9.18","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"NixOS","version":"25.11","id":"xantusia","libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}
|
