Skip to main content

A python library for manipulating sequential and-inverter gates.

Project description

<figure> py-aiger logo <figcaption> pyAiger: A python library for manipulating sequential and combinatorial circuits. </figcaption> </figure>

Build Status codecov Updates

PyPI version License: MIT DOI

Table of Contents

About PyAiger

  1. Q: How is Py-Aiger pronounced? A: Like "pie" + "grrr".
  2. Q: Why python? Aren't you worried about performance?! A: No. The goals of this library are ease of use and hackability.
  3. 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.
  4. 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 austrian mountain Eiger.

Installation

If you just need to use aiger, you can just run:

$ pip install py-aiger

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

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.atom('x'), aiger.atom('y'), aiger.atom('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 & aiger.atom(True)  # Equivilent to just x.
expr9 = x & aiger.atom(False)  # Equivilent to const False.

# 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/Feedback/Delay

# Connect output y to input x with delay, initialized to True.
# (Default initialization is False.)
aig5 = aig1.feedback(
    inputs=['x'],
    outputs=['y'],
    initials=[True],
    keep_outputs=True
)

Relabeling

# Relabel input 'x' to 'z'.
aig1['i', {'x': 'z'}]

# Relabel output 'y' to 'w'.
aig1['o', {'y': 'w'}]

# Relabel latches 'l1' to 'l2'.
aig1['l', {'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']})

# Make an AND gate.
aiger.and_gate(['x', 'y'], out='name')

# Make an OR gate.
aiger.or_gate(['x', 'y'])  # Default output name is #or_output.

# And outputs.
aig1 >> aiger.and_gate(aig1.outputs) # Default output name is #and_output.

# Or outputs.
aig1 >> aiger.or_gate(inputs=aig1.outputs, output='my_output')

# Flip outputs.
aig1 >> aiger.bit_flipper(inputs=aig1.outputs)

# Flip inputs.
aiger.bit_flipper(inputs=aig1.inputs) >> aig1

# ITE circuit
# ['o1', 'o2'] = ['i1', 'i2'] if 'test' Else ['i3', 'i4'] 
aiger.common.ite('test', ['i1', 'i2'], ['i3', 'i4'], outputs=['o1', 'o2'])

Extra

eval_order(aig1)  # Returns topological ordering of circuit gates.

Ecosystem

<figure> py-aiger ecosystem <figcaption>Overview of the pyaiger ecosystem/stack.</figcaption> </figure>

Stable

Stay tuned!

Underdevelopment

  • py-aiger-bv: Extension of pyAiger for manipulating sequential bitvector circuits.
  • py-aiger-bdd: Aiger <-> BDD bridge.
  • py-aiger-past-ltl: Converts Past Linear Temporal Logic to aiger circuits.
  • py-aiger-gridworld: Create aiger circuits representing gridworlds.
  • py-aiger-spectral: A tool for performing (Fourier) Analysis of Boolean Functions.
  • py-aigar: pyAiger-Analysis: Batteries included tools for analyzing aiger circuits.

Related Projects

  • pyAig: Another python library for working with AIGER circuits.

Citing

@misc{pyAiger,
  author       = {Marcell Vazquez-Chanlatte},
  title        = {mvcisback/py-aiger},
  month        = aug,
  year         = 2018,
  doi          = {10.5281/zenodo.1326224},
  url          = {https://doi.org/10.5281/zenodo.1326224}
}

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Filename, size & hash SHA256 hash help File type Python version Upload date
py_aiger-3.3.3-py3-none-any.whl (17.0 kB) Copy SHA256 hash SHA256 Wheel py3
py-aiger-3.3.3.tar.gz (18.0 kB) Copy SHA256 hash SHA256 Source None

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page