pyAiger-BV: Extension of pyAiger for manipulating sequential bitvector circuits.

About Py-Aiger-BV

This library provides word level abstractions on top of py-aiger. This is done by the AIGBV which groups inputs, outputs, and latches into named ordered sequences, e.g. bitvectors.

The resulting objects can be turned into AIGs where each input, output, or latches name has its index appended to its name. For example, an bitvector input, 'x' with 3 bits becomes inputs 'x[0]', 'x[1]', 'x[3]'

Installation

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

$ pip install py-aiger-bv

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

$ poetry install

BitVector Expression DSL

As in py-aiger, when writing combinatorial circuits, the Sequential Circuit DSL can be somewhat clumsy. For this common usecase, we have developed the BitVector Expression DSL. This DSL actually consists of two DSLs for signed and unsigned BitVectors. All circuits generated this way have a single output word. We use a big-endian encoding where the most significant digit is the first element of the tuple representing the word. For signed numbers, two's complement is used.

import aiger_bv

# Create 16 bit variables.
x = aiger_bv.atom(16, 'x')
y = aiger_bv.atom(16, 'y', signed=True)  # Signed by default.
z = aiger_bv.uatom(16, 'z')              # Equiv to signed=False.

# bitwise ops.
expr1 = x & y  # Bitwise and.
expr2 = x | y  # Bitwise or.
expr3 = x ^ y  # Bitwise xor.
expr4 = ~x  # Bitwise negation.

# arithmetic
expr5 = x + y
expr6 = x - y
expr7 = x << y
expr8 = x >> y  # logical if unsigned, arithmetic if signed.
expr9 = -x  # Arithmetic negation. Only defined for signed expr.
expr10 = abs(x)
expr11 = x @ y  # inner product of bitvectors mod 2 (+ is xor).

# comparison
expr12 = x == y
expr13 = x != y
expr14 = x < y
expr15 = x <= y
expr16 = x > y
expr17 = x >= y

# Atoms can be constants.
expr18 = x & aiger_bv.atom(16, 3)
expr19 = x & aiger_bv.atom(16, 0xff)

# BitVector expressions can be concatenated.
expr20 = x.concat(y)

# Particular bits can be indexed to create new expressions.
expr21 = x[1]

# Single bit expressions can be repeated.
expr22 = x[1].repeat(10)

# And you can inspect the AIGBV if needed.
circ = x.aigbv

# And you can inspect the AIG if needed.
circ = x.aigbv.aig

# And of course, you can get a BoolExpr from a single output aig.
expr = aiger_bv.UnsignedBVExpr(circ)

Sequential Circuit DSL

py-aiger-bv's Sequential Circuit DSL implements the same basic api as py-aiger's Sequential Circuit DSL, but operates at the (variable length) word level rather than the bit level.

import aiger
import aiger_bv


circ = ... # Create a circuit (see below).

# We assume this circuit has word level
# inputs: x,y, outputs: z, w, q, latches: a, b
assert circ.inputs == {'x', 'y'}
assert circ.outputs == {'z', 'w', 'q'}
assert circ.latches == {'a', 'b'}

Sequential composition

circ3 = circ1 >> circ2

Parallel composition

circ3 = circ1 | circ2

Adding Feedback (inserts a delay)

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

Relabeling

# Relabel input 'x' to 'z'.
circ2 = circ['i', {'x': 'z'}]

# Relabel output 'y' to 'w'.
circ2 = circ['o', {'y': 'w'}]

# Relabel latches 'l1' to 'l2'.
circ2 = circ['l', {'l1': 'l2'}]

Evaluation

# Combinatoric evaluation.
circ(inputs={'x':(True, False, True), 'y': (True, False)})

# Sequential evaluation.
circ.simulate([
        {'x': (True, False, True), 'y': (True, False)},
        {'x': (False, False, True), 'y': (False, False)},
    ])

# Simulation Coroutine.
sim = circ.simulator()  # Coroutine
next(sim)  # Initialize
print(sim.send({'x': (True, False, True), 'y': (True, False)}))
print(sim.send({'x': (False, False, True), 'y': (False, False)}))


# Unroll
circ2 = circ.unroll(steps=10, init=True)

aiger.AIG to aiger.AIGBV

There are two main ways to take an object AIG from aiger and convert it into an AIGBV object. The first is the aig2aigbv command which simply makes all inputs words of size 1.

# Create aiger_bv.AIGERBV object from aiger.AIG object.
circ  = ... # Some aiger.AIG object
word_circ = aiger_bv.aig2aigbv(circ)  # aiger_bv.AIGBV object

Gadget Library

General Manipulation

# Copy outputs 'x' and 'y' to 'w1, w2' and 'z1, z2'.
circ1 = circ >> aiger_bv.tee(wordlen=3, iomap={
        'x': ('w1', 'w2'),
        'y': ('z1', 'z2')
    })

# Take 1 bit output, 'x', duplicate it 5 times, and group into
# a single 5-length word output, 'y'.
circ2 = circ >> aiger_bv.repeat(wordlen=5, input='x', output='z')

# Reverse order of a word.
circ3 = circ >> aiger_bv.reverse_gate(wordlen=5, input='x', output='z')

# Sink and Source circuits (see encoding section for encoding details).
## Always output binary encoding for 15. 
circ4 = aiger_bv.source(wordlen=4, value=15, name='x', signed=False)

## Absorb output 'y'
circ5 = circ >> aiger_bv.sink(wordlen=4, inputs=['y'])

# Identity Gate
circ6 = circ >> aiger_bv.identity_gate(wordlen=3, input='x')

# Combine/Concatenate words
circ7 = circ >> aiger_bv.combine_gate(
    left_wordlen=3, left='x',
    right_wordlen=3, right='y',
    output='z'
)

# Split words
circ8 = circ >> aiger_bv.split_gate(
    input='x',
    left_wordlen=1, left='z',
    right_wordlen=2, right='w'
)

# Select single index of circuit and make it a wordlen=1 output.
circ9 = circ >> aiger_bv.index_gate(wordlen=3, idx=1, input='x', output='x1')

Bitwise Operations

aiger_bv.bitwise_and(3, left='x', right='y', output='x&y')
aiger_bv.bitwise_or(3, left='x', right='y', output='x|y')
aiger_bv.bitwise_xor(3, left='x', right='y', output='x^y')
aiger_bv.bitwise_negate(3, left='x', output='~x')

Arithmetic

aiger_bv.add_gate(3, left='x', right='y', output='x+y')
aiger_bv.subtract_gate_gate(3, left='x', right='y', output='x-y')
aiger_bv.inc_gate(3, left='x', output='x+1')
aiger_bv.dec_gate(3, left='x', output='x+1')
aiger_bv.negate_gate(3, left='x', output='-x')
aiger_bv.logical_right_shift(3, shift=1, input='x', output='x>>1')
aiger_bv.arithmetic_right_shift(3, shift=1, input='x', output='x>>1')
aiger_bv.left_shift(3, shift=1, input='x', output='x<<1')

Comparison

aiger_bv.is_nonzero_gate(3, input='x', output='is_nonzero')
aiger_bv.is_zero_gate(3, input='x', output='is_zero')
aiger_bv.eq_gate(3, left='x', right='y', output='x=y')
aiger_bv.ne_gate(3, left='x', right='y', output='x!=y')
aiger_bv.unsigned_lt_gate(3, left='x', right='y', output='x<y')
aiger_bv.unsigned_gt_gate(3, left='x', right='y', output='x>y')
aiger_bv.unsigned_le_gate(3, left='x', right='y', output='x<=y')
aiger_bv.unsigned_ge_gate(3, left='x', right='y', output='x>=y')
aiger_bv.signed_lt_gate(3, left='x', right='y', output='x<y')
aiger_bv.signed_gt_gate(3, left='x', right='y', output='x>y')
aiger_bv.signed_le_gate(3, left='x', right='y', output='x<=y')
aiger_bv.signed_ge_gate(3, left='x', right='y', output='x>=y')

Metadata

Release files for py-aiger-bv 4.7.8

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for py-aiger-bv 4.7.8
File	Size	Uploaded	Provenance
py_aiger_bv-4.7.8.tar.gz	16.3 kB	Dec 21, 2024	Without provenance	Details

Built distribution (wheel)

Table of built distributions (wheels) for py-aiger-bv 4.7.8
File	Interpreter	ABI	Platform	Reset
py_aiger_bv-4.7.8-py3-none-any.whl 15.5 kB Dec 21, 2024 Without provenance	Python 3	none	any	Details

Total release size: 31.8 kB

Release files / py_aiger_bv-4.7.8.tar.gz

Download URL	py_aiger_bv-4.7.8.tar.gz
Size	16.3 kB
Tags	Source
SHA-256 checksum How to use checksums	`68a20057b3609ab18bcba872cd8ce5fca7e6f218a33f080c06affd5c24bb97c8`
BLAKE2b-256 checksum How to use checksums	`7226da15f693c057942eed37e5a2b5d5105a981915a3fd13663bc013586f2427`
Upload date	Dec 21, 2024
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`poetry/1.8.4 CPython/3.12.7 Linux/6.11.1`

Release files / py_aiger_bv-4.7.8-py3-none-any.whl

Download URL	py_aiger_bv-4.7.8-py3-none-any.whl
Size	15.5 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`6aac5d9a5f80f7b3321610da7021403a519edb5efd9866cd8828295b93aa62c8`
BLAKE2b-256 checksum How to use checksums	`33c5f67d82e3016363bfed9d6f738d1440c16796b6f939eb47255dd843e49eba`
Upload date	Dec 21, 2024
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`poetry/1.8.4 CPython/3.12.7 Linux/6.11.1`

Security for py-aiger-bv 4.7.8

Report project as malware

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.