Library for moving between sequential circuits AIGs and DFAs.

# py-aiger-dfa

Python library for converting between AIG circuits and DFAs.

# Installation

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

$pip install py-aiger-dfa For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run: $ poetry install

# Usage

The main entry points for using this library are the dfa2aig and aig2dfa functions. DFAs are represented using the dfa package. Familiarity with the dfa, py-aiger, and py-aiger-bv packages is assumed.

## DFA to AIG

An example of going from a DFA to an AIG object is shown below.

from dfa import DFA
from aiger_dfa import dfa2aig

my_dfa = DFA(
start=0,
inputs={0, 1},
label=lambda s: (s % 4) == 3,
transition=lambda s, c: (s + c) % 4,
)
my_aig, relabels, valid = dfa2aig(my_dfa)


Now circ is an AIG and relabels is a mapping from the inputs, states, and outputs of my_dfa to their 1-hot encoded counterparts in my_aig.

relabels has the following schema:

relabels = {
'inputs': .. , #  Mapping from input alphabet -> py-aiger input.
'outputs': .. , # Mapping from py-aiger output -> output alphabet.
'states': .. , # Mapping from state space -> py-aiger latches.
}


Finally, valid is another aiger circuit which tests if all inputs are 1-hot encoded.

## AIG to DFA

We also support converting a sequential circuit (AIG) to a Moore Machine (DFA) using aig2dfa. Using the same example:

from aiger_dfa import aig2dfa

my_dfa2 = aig2dfa(my_aig, relabels=relabels)


Note that the output of a sequential circuit (AIG) is dependent on the state AND the action (a Mealy Machine).

We use the standard Mealy ↦ Moore reduction where one introduces a 1-step delay on the output. The default initial output is None, but can be set using the initial_label argument.

## Project details

Uploaded source
Uploaded py3