diff options
Diffstat (limited to 'python-py-aiger-bv.spec')
| -rw-r--r-- | python-py-aiger-bv.spec | 904 |
1 files changed, 904 insertions, 0 deletions
diff --git a/python-py-aiger-bv.spec b/python-py-aiger-bv.spec new file mode 100644 index 0000000..55793e0 --- /dev/null +++ b/python-py-aiger-bv.spec @@ -0,0 +1,904 @@ +%global _empty_manifest_terminate_build 0 +Name: python-py-aiger-bv +Version: 4.7.6 +Release: 1 +Summary: A python library for manipulating sequential and-inverter gates. +License: MIT +URL: https://pypi.org/project/py-aiger-bv/ +Source0: https://mirrors.nju.edu.cn/pypi/web/packages/c7/3c/3aa329f97ad2e8b2e020eeefca22189931e8d1fba4f59387b9b1aff389db/py_aiger_bv-4.7.6.tar.gz +BuildArch: noarch + +Requires: python3-attrs +Requires: python3-funcy +Requires: python3-py-aiger +Requires: python3-pyrsistent + +%description +<figure> + <img src="logo_text.svg" alt="py-aiger-bv logo" width=300px> + <figcaption>pyAiger-BV: Extension of pyAiger for manipulating + sequential bitvector circuits.</figcaption> +</figure> + + +[](https://cloud.drone.io/mvcisback/py-aiger-bv) +[](https://mvcisback.github.io/py-aiger-bv) +[](https://badge.fury.io/py/py-aiger-bv) +[](https://opensource.org/licenses/MIT) + +# Table of Contents +- [About](#about-py-aiger-bv) +- [Installation](#installation) +- [BitVector Expr DSL](#bitvector-expression-dsl) +- [Sequential Circuit DSL](#sequential-circuit-dsl) + +# About Py-Aiger-BV + +This library provides word level abstractions on top of +[py-aiger](https://github.com/mvcisback/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 `AIG`s 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](https://poetry.eustace.io/) 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. + +```python +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. + +```python +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 +```python +circ3 = circ1 >> circ2 +``` + +## Parallel composition +```python +circ3 = circ1 | circ2 +``` + +## Adding Feedback (inserts a delay) +```python +# 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 +```python +# 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 +```python +# 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. + + +```python +# 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 + +```python +# 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')` + + +%package -n python3-py-aiger-bv +Summary: A python library for manipulating sequential and-inverter gates. +Provides: python-py-aiger-bv +BuildRequires: python3-devel +BuildRequires: python3-setuptools +BuildRequires: python3-pip +%description -n python3-py-aiger-bv +<figure> + <img src="logo_text.svg" alt="py-aiger-bv logo" width=300px> + <figcaption>pyAiger-BV: Extension of pyAiger for manipulating + sequential bitvector circuits.</figcaption> +</figure> + + +[](https://cloud.drone.io/mvcisback/py-aiger-bv) +[](https://mvcisback.github.io/py-aiger-bv) +[](https://badge.fury.io/py/py-aiger-bv) +[](https://opensource.org/licenses/MIT) + +# Table of Contents +- [About](#about-py-aiger-bv) +- [Installation](#installation) +- [BitVector Expr DSL](#bitvector-expression-dsl) +- [Sequential Circuit DSL](#sequential-circuit-dsl) + +# About Py-Aiger-BV + +This library provides word level abstractions on top of +[py-aiger](https://github.com/mvcisback/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 `AIG`s 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](https://poetry.eustace.io/) 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. + +```python +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. + +```python +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 +```python +circ3 = circ1 >> circ2 +``` + +## Parallel composition +```python +circ3 = circ1 | circ2 +``` + +## Adding Feedback (inserts a delay) +```python +# 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 +```python +# 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 +```python +# 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. + + +```python +# 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 + +```python +# 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')` + + +%package help +Summary: Development documents and examples for py-aiger-bv +Provides: python3-py-aiger-bv-doc +%description help +<figure> + <img src="logo_text.svg" alt="py-aiger-bv logo" width=300px> + <figcaption>pyAiger-BV: Extension of pyAiger for manipulating + sequential bitvector circuits.</figcaption> +</figure> + + +[](https://cloud.drone.io/mvcisback/py-aiger-bv) +[](https://mvcisback.github.io/py-aiger-bv) +[](https://badge.fury.io/py/py-aiger-bv) +[](https://opensource.org/licenses/MIT) + +# Table of Contents +- [About](#about-py-aiger-bv) +- [Installation](#installation) +- [BitVector Expr DSL](#bitvector-expression-dsl) +- [Sequential Circuit DSL](#sequential-circuit-dsl) + +# About Py-Aiger-BV + +This library provides word level abstractions on top of +[py-aiger](https://github.com/mvcisback/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 `AIG`s 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](https://poetry.eustace.io/) 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. + +```python +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. + +```python +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 +```python +circ3 = circ1 >> circ2 +``` + +## Parallel composition +```python +circ3 = circ1 | circ2 +``` + +## Adding Feedback (inserts a delay) +```python +# 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 +```python +# 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 +```python +# 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. + + +```python +# 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 + +```python +# 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')` + + +%prep +%autosetup -n py-aiger-bv-4.7.6 + +%build +%py3_build + +%install +%py3_install +install -d -m755 %{buildroot}/%{_pkgdocdir} +if [ -d doc ]; then cp -arf doc %{buildroot}/%{_pkgdocdir}; fi +if [ -d docs ]; then cp -arf docs %{buildroot}/%{_pkgdocdir}; fi +if [ -d example ]; then cp -arf example %{buildroot}/%{_pkgdocdir}; fi +if [ -d examples ]; then cp -arf examples %{buildroot}/%{_pkgdocdir}; fi +pushd %{buildroot} +if [ -d usr/lib ]; then + find usr/lib -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/lib64 ]; then + find usr/lib64 -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/bin ]; then + find usr/bin -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/sbin ]; then + find usr/sbin -type f -printf "/%h/%f\n" >> filelist.lst +fi +touch doclist.lst +if [ -d usr/share/man ]; then + find usr/share/man -type f -printf "/%h/%f.gz\n" >> doclist.lst +fi +popd +mv %{buildroot}/filelist.lst . +mv %{buildroot}/doclist.lst . + +%files -n python3-py-aiger-bv -f filelist.lst +%dir %{python3_sitelib}/* + +%files help -f doclist.lst +%{_docdir}/* + +%changelog +* Thu May 18 2023 Python_Bot <Python_Bot@openeuler.org> - 4.7.6-1 +- Package Spec generated |