py-aiger-dfa

Python library for converting between AIG circuits and DFAs.

Table of Contents

• Installation
• Usage
  • DFA to AIG
  • AIG to DFA

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.