[Synth][AIG][BLIF] Adding new Synth Dialect and BLIF Importer and Exporter (#756)

The following PR adds a new dialect Synth to represent AIG at MLIR
level.

Additionally, it adds two new passes to import a BLIF file and represent
it with the Synth dialect and to convert the Synth Dialect into a BLIF
file.

For more information related to this PR, please look at the newly added
docs.

Author: Carmine50

.github/workflows/unittests.yml

@@ -0,0 +1,64 @@
+name: unittests
+
+on:
+  # Make sure that settings are set to require permission
+  # to run workflows by external contributors!
+  pull_request:
+    paths-ignore:
+      - 'docs/**'
+    branches: ["main"]
+    types: [opened, synchronize, reopened, ready_for_review]
+  
+  push:
+    paths-ignore:
+      - 'docs/**'
+    branches: ["main"]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  unittests:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: cleanup
+        run: |
+          echo "Emptying folder"
+          rm -rf -- * .*
+          echo "Folder contents"
+          ls -la
+
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Update apt and install prerequisites
+        run: |
+          sudo apt-get -y update
+          sudo apt-get -y install software-properties-common
+          sudo add-apt-repository ppa:deadsnakes/ppa
+
+      - name: Install system dependencies
+        run: |
+          sudo apt-get install -y \
+            --option APT::Immediate-Configure=false \
+            sudo vim clang lld ccache cmake wget \
+            ninja-build python3 graphviz git curl \
+            gzip libreadline-dev \
+            libboost-all-dev pkg-config python3.12 \
+            python3.12-venv python3.12-dev \
+            ghdl verilator
+
+      - name: Verify Python 3.12
+        run: python3.12 --version
+
+      - name: build
+        run: ./build.sh --release --use-prebuilt-llvm --enable-abc --enable-cbc --force
+
+      - name: check-blif-importer-exporter
+        if: steps.build.outputs.exit_code == 0
+        run: ninja run-blif-equiv-tests
+        working-directory: build
+
+

CMakeLists.txt

@@ -245,6 +245,32 @@ if(DYNAMATIC_ENABLE_CBC)
   endif()
 endif()
 
+#-------------------------------------------------------------------------------
+# ABC setup
+#-------------------------------------------------------------------------------
+
+if(DYNAMATIC_ENABLE_ABC)
+  if (UNIX)
+
+    # Disable reproducibility warning for third-party code
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-error=date-time -Wno-date-time")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-error=date-time -Wno-date-time")
+
+    FetchContent_Declare(
+      abc
+      DOWNLOAD_EXTRACT_TIMESTAMP TRUE
+      SOURCE_DIR ${CMAKE_BINARY_DIR}/abc
+      URL https://github.com/ETHZ-DYNAMO/abc/archive/refs/tags/v1.0.0.tar.gz
+      SYSTEM
+    )
+
+    FetchContent_MakeAvailable(abc)
+    add_compile_definitions(DYNAMATIC_ENABLE_ABC)
+  else()
+    message(FATAL_ERROR "ABC integration is not tested on the OS you use!")
+  endif()
+endif()
+
 #-------------------------------------------------------------------------------
 # Python (Virtual Environment)
 #-------------------------------------------------------------------------------

build.sh

@@ -30,6 +30,7 @@ List of options:
                                          checking
   --use-prebuilt-llvm                  : download and use the prebuilt LLVM
   --enable-cbc                         : enable the CBC milp solver
+  --enable-abc                         : enable the ABC logic synthesis tool
   --build-legacy-lsq                   : build the legacy chisel-based lsq
   --check | -c                         : run tests during build
   --help | -h                          : display this help message
@@ -143,6 +144,7 @@ PREBUILT_LLVM=0
 BUILD_CHIESEL_LSQ=0
 ENABLE_CBC=0
 CMAKE_DYNAMATIC_ENABLE_CBC=""
+CMAKE_DYNAMATIC_ENABLE_ABC=""
 LLVM_DIR="$PWD/llvm-project/build"
 
 # Loop over command line arguments and update script variables
@@ -206,6 +208,9 @@ do
               CMAKE_DYNAMATIC_ENABLE_CBC="-DDYNAMATIC_ENABLE_CBC=ON"
               ENABLE_CBC=1
               ;;
+          "--enable-abc")
+              CMAKE_DYNAMATIC_ENABLE_ABC="-DDYNAMATIC_ENABLE_ABC=ON"
+              ;;
           "--build-legacy-lsq")
               BUILD_CHIESEL_LSQ=1
               ;;
@@ -359,6 +364,7 @@ if should_run_cmake ; then
             $CMAKE_LLVM_BUILD_OPTIMIZATIONS \
             $CMAKE_DYNAMATIC_ENABLE_XLS \
             $CMAKE_DYNAMATIC_ENABLE_CBC \
+            $CMAKE_DYNAMATIC_ENABLE_ABC \
             $CMAKE_DYNAMATIC_ENABLE_LEQ_BINARIES
 
     LLVM_DIR="../build/llvm-project"
@@ -375,6 +381,7 @@ if should_run_cmake ; then
         $CMAKE_DYNAMATIC_BUILD_OPTIMIZATIONS \
         $CMAKE_DYNAMATIC_ENABLE_XLS \
         $CMAKE_DYNAMATIC_ENABLE_CBC \
+        $CMAKE_DYNAMATIC_ENABLE_ABC \
         $CMAKE_DYNAMATIC_ENABLE_LEQ_BINARIES
   fi
   exit_on_fail "Failed to cmake dynamatic"
@@ -458,12 +465,14 @@ create_symlink ../build/bin/dynamatic
 create_symlink ../build/bin/dynamatic-mlir-lsp-server
 create_symlink ../build/bin/dynamatic-opt
 create_symlink ../build/bin/elastic-miter
+create_symlink ../build/bin/export-blif
 create_symlink ../build/bin/export-dot
 create_symlink ../build/bin/export-cfg
 create_symlink ../build/bin/export-rtl
 create_symlink ../build/bin/exp-frequency-profiler
 create_symlink ../build/bin/handshake-simulator
 create_symlink ../build/bin/hls-verifier
+create_symlink ../build/bin/import-blif
 create_symlink ../build/bin/log2csv
 create_symlink "../build/bin/rigidification-testbench"
 create_generator_symlink build/bin/rtl-cmpf-generator

docs/DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/BlifExporter.md

@@ -0,0 +1,63 @@
+# BLIF Exporter
+
+The **BLIF Exporter** is an binary that serializes a Synth dialect circuit contained inside `hw.module` operations into a BLIF file. It serves as the inverse of the BLIF Importer, allowing Dynamatic's IR to be exported back to a standard BLIF representation for use with external synthesis tools.
+
+---
+
+## Code Structure
+
+The binary `export-blif` can be called as follows:
+```bash
+./bin/export-blif <input-mlir-file> <output-blif-file>
+```
+
+where `input-mlir-file` is the file that contains the Synth circuit to be exported and `output-blif-file` is the file containing the exported BLIF.
+
+The core functionality is the following:
+
+- It iterates over all `hw.HWModuleOp` operations in the module and calls `exportBlifCircuit` on each of them to generate a BLIF module.
+
+The core function `exportBlifCircuit` executes the following steps:
+
+1. It writes the `.model`, `.inputs`, and `.outputs` lines, and collects all port names into the `inputPorts` and `outputPorts` vectors using the `generateBlifHeader` function.
+2. It iterates over the ops inside the module body and emit the corresponding BLIF statements using the `generateBlifCircuitFromSynth` function.
+3. Writes the `.end` terminator to close the BLIF model.
+
+---
+
+## Support Functions
+
+In this subsection of the doc, we highlight the key support functions.
+
+### Generate BLIF Header
+
+The core function that writes the header section of the BLIF file for a given `hw.HWModuleOp` is `generateBlifHeader`. It:
+
+1. Writes the `.model` line using the `hw.module` name.
+2. Iterates over the module's port list and writes all input ports on the `.inputs` line. It populates the vector `inputPorts` which contains the same list.
+3. Iterates over the module's port list and writes all output ports on the `.outputs` line. It populates the vector `outputPorts` which contains the same list.
+
+### Generate BLIF Functionality 
+
+The core function that translates the Synth operations inside an `hw.HWModuleOp` into BLIF statements is `generateBlifCircuitFromSynth`. It iterates over all ops in the module body and handles three operation types:
+
+- **`synth.latch`**: the function emits a `.latch` statement with the format `.latch <input> <output> [type control] [init]`. The input and output operand names are resolved via `getValueName`. Optional fields are emitted only when present: if a control signal exists, the latch type (defaulting to `"re"` if unset) and control signal name are written; if an init value is set, it is appended.
+
+- **`synth.aig.and_inv`**: the function emits a `.names` statement listing both input operand names and the output result name, followed by a truth-table row. Each input position in the row is `"0"` if that input is inverted and `"1"` otherwise.
+
+- **`hw.constant`**: the function emits a single-node `.names` statement (`.names <output>`) followed by either `1` or `0` on the next line, corresponding to the constant's value. Only 1-bit constants are supported.
+
+- **`hw.output`**: after all ops are processed, the function checks whether any output port is directly connected to an input port (i.e., a pass-through with no Synth op in between). For each such case, a two-node `.names` wire statement is emitted (`1 1`), connecting the input port name to the output port name. At the end, the function asserts that every output port has been accounted for.
+
+Any other operation type is reported as unsupported via an error message.
+
+
+### Value Naming in BLIF
+
+Value names in the BLIF output are resolved by the internal `getValueName` lambda, which applies the following priority:
+
+1. If the value is a block argument (input port), return its name from `inputPorts` using the argument index.
+2. If the value is used as an operand of `hw.output` (output port), return its name from `outputPorts` using the operand index offset by the number of input ports.
+3. Otherwise, print the value using MLIR's `AsmState` (e.g., `%4`), strip the leading `%`, and prepend `n` to produce a valid BLIF node name (e.g., `n4`).
+
+This function ensure uniqueness and consistency of names inside a BLIF module.

docs/DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/BlifImporter.md

@@ -0,0 +1,77 @@
+# Blif Importer
+
+
+The BLIF Importer is a binary that reads a BLIF file and generates a corresponding Synth dialect circuit inside an `hw.module`. It serves as a standalone entry point for importing externally synthesized logic directly into Dynamatic's IR.
+
+This code interprets each BLIF model as an AIG-style circuit composed of 1-bit registers and AND-with-inverter gates, and re-expresses it directly in the Synth dialect while preserving the instance’s interface.
+
+---
+
+## Code Structure
+
+The binary `import-blif` can be called as follows:
+```bash
+./bin/export-blif <output-mlir-file> <intput-blif-file>
+```
+
+where `output-mlir-file` is the file that will contain the Synth circuit to be imported and `input-blif-file` is the file containing imported BLIF.
+
+The code core function is `importBlifCircuit(moduleOp, loc, blifFilePath)` which imports the blif specified in `blifFilePath` in the module operation `moduleOp`.
+
+This function executes the following steps:
+
+1. Extract the module name, input and output port names of the module from the BLIF file using the `getBlifModuleHeader` function.
+2. Create an hw module operation `hw.HWModuleOp` with input and output ports corresponding to the one of the model described in the BLIF file using the `createHWModuleShell`.
+3. Create all synth operations inside the `hw.HWModuleOp` using the function `populateHWModuleShell`. Then, attach all the outputs of the synth circuit to the terminator of the `hw.HWModuleOp`.
+
+---
+
+## Support Functions
+
+In this subsection of the doc, we highlight the key support functions.
+
+
+### Generate Synth Operations
+
+The core function to generate synth operations is `populateHWModuleShell`. It parses the BLIF body line by line and emits the corresponding Synth operations. It maintains two maps throughout:
+
+- `nodeValuesMap` which maps a BLIF node name to its Synth Value. Pre-populated with all input port signals before parsing begins.
+- `tmpValuesMap` which maps a BLIF node name to a temporary `hw.constant 0` placeholder, created when a node's output is referenced before defining the node. Placeholders are replaced and erased once the real value is available.
+
+**IMPORTANT**: `tmpValuesMap` may contain a large number of temporary `hw` constants which should be cleaned up during synth graph construction. For BLIF generated by tools such as [ABC](https://github.com/berkeley-abc/abc), these temporaries arise primarily from latches since since latches appear at the start of the BLIF file and their inputs are not yet defined at generation time. As a result, performance impact scales mainly with latch count.
+
+It handles two types of units defined in the BLIF:
+
+1. `.latch` from which it parses input node, output node, and oprtional fields (`latchType`, `controlName`, `initVal`). The optional fields follow the BLIF syntax `[type control] [init]` and are decoded based on the number of tokens. A `synth.latch` of type `i1` is created and registered via `updateOutputSynthSignalMapping` in order to record its output value.
+2. `.names` from which it parses the input and output node names and the truth-table function. Depending on the number of node names, the behaviour is different:
+  - 1 node name: it is a constant and an `hw.constant` is generated
+  - 2 node names: it is a wire or an inverter and it is handled by `createSynthWire`
+  - 3+ node names: it is a logic gate and it is handled by `createSynthLogicGate`
+
+After parsing, all the outputs of the synth circuit are appended in the `synthOutputs` variable.
+
+
+### Retrieve the Value of the Input of a BLIF Node
+
+The function that retrieves the input of a synth node is `getInputMappingSynthSignal`. It resolves a BLIF node name to a Synth Value applying the following steps:
+
+1. Return the value from `nodeValuesMap` if already defined.
+2. Return the existing placeholder from `tmpValuesMap` if one exists.
+3. Create a new `hw.constant 0` placeholder, store it in `tmpValuesMap`, and return it.
+
+### Save the Value of the Output of a BLIF Node
+
+The function that saves the MLIR Value corresponding to the output of a BLIF node is `updateOutputSynthSignalMapping`. It registers  a newly created Synth value as the definitive signal for a given node name. If a temporary placeholder exists in `tmpValuesMap` for that name, all its uses are replaced with the new value, its defining `hw.constant` op is erased, and it is removed from `tmpValuesMap`. The new value is then recorded in `nodeValuesMap`.
+
+### Create a Wire
+
+The function that creates a wire in the Synth circuit is `createSynthWire`. It handles two-node `.names` blocks. Compares the input and output bits of the truth-table function string (format: "X Y"):
+
+- If equal, the output node is aliased directly to the input value via `updateOutputSynthSignalMapping` and no new op is created.
+- If different, a `synth.aig.and_inv` is created with the input inverted and `ANDed` with a constant 1, effectively modelling a NOT gate.
+
+### Create a Logic Gate
+
+The function that creates a logic gate in the Synth circuit is `createSynthLogicGate`. It handles multi-input `.names` blocks. Currently asserts that exactly 2 inputs are present, reflecting that the code operates on already-binarized AIG-form BLIF. The truth-table function string (format: "XY Z") determines the inversion flags for each input. A `synth.aig.and_inv` is created with the appropriate inversion flags. If the output bit is `0`, a second `synth.aig.and_inv` ANDing with constant 1 and inverting the first input is appended to negate the result.
+
+

docs/DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/Synth.md

@@ -0,0 +1,45 @@
+# Synth dialect
+
+
+The **Synth** dialect is a low-level synthesis-oriented dialect that provides a common in-MLIR interface for logic synthesis operations and data structures. It is intended as an intermediate representation between higher-level hardware IR (e.g., Handshake or HW) and concrete synthesis backends, capturing both logic networks (such as AIGs) and meta-operations that steer synthesis decisions.
+
+In Dynamatic, operations of the synth dialect are always described inside an `hw.module` operation of the hw dialect.
+
+---
+
+## Design and role in the flow
+
+The Synth dialect has a core responsibility:
+
+- Support **logic network representations** such as AIG (And-Inverter Graph) and sequential elements as latches.
+
+In other words, the Synth dialect is not tied to a particular hardware backend or HDL; instead, it serves as an abstraction layer where logic-level manipulations can be expressed, analyzed, and transformed before being committed to a specific RTL or gate-level format.
+
+---
+
+## Operations 
+
+This dialect describes two core operations:
+
+- `AndInverterOp` which describes the nodes of an AIG.
+- `LatchOp` which describes the presence of a latch.
+
+### And-Inverter Node
+
+It represents a node in an AIG. It computes the bitwise AND of all inputs, each of which may be individually inverted. 
+
+```mlir
+%r1 = synth.aig.and_inv %a, %b : i1
+%r2 = synth.aig.and_inv not %a, %b : i1
+%r3 = synth.aig.and_inv not %a, not %b : i1
+```
+
+### Latch Node 
+
+It models a storage element, directly corresponding to the BLIF `.latch` construct. Accepts three optional parameters: a `latchType` string ("fe", "re", "ah", "al", "as"), a control clock/enable signal, and an initVal encoding the initial state (0, 1, 2 = don't care, 3 = unknown).
+
+```mlir
+%q = synth.latch %d : i1
+%q = synth.latch %d clock %clk init 0 : i1
+```
+

docs/SUMMARY.md

@@ -77,6 +77,10 @@
     - [Commit Unit Placement Algorithm](DeveloperGuide/DynamaticFeaturesAndOptimizations/Speculation/CommitUnitPlacementAlgorithm.md)
     - [Integration Tests](DeveloperGuide/DynamaticFeaturesAndOptimizations/Speculation/IntegrationTests.md)
     - [Save Commit Behavior](DeveloperGuide/DynamaticFeaturesAndOptimizations/Speculation/SaveCommitBehavior.md)
+  - [Synth]()
+    - [Synth Dialect](DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/Synth.md)
+    - [Blif Importer](DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/BlifImporter.md)
+    - [Blif Exporter](DeveloperGuide/DynamaticFeaturesAndOptimizations/Synth/BlifExporter.md)
 
 - [Specs]()
   - [Floating Point Units](DeveloperGuide/Specs/FloatingPointUnits.md)

experimental/tools/elastic-miter/CMakeLists.txt

@@ -18,6 +18,7 @@ target_link_libraries(elastic-miter
   DynamaticSupport
   DynamaticTransforms
   DynamaticExperimentalSupport
+  DynamaticSynth
 
   MLIRIR
   MLIRMemRefTransforms

experimental/tools/rigidification/CMakeLists.txt

@@ -11,6 +11,7 @@ target_link_libraries(rigidification-testbench
   PRIVATE
   DynamaticHandshake
   DynamaticExperimentalSupport
+  DynamaticSynth
 
   MLIRIR
   MLIRMemRefTransforms

include/dynamatic/Dialect/CMakeLists.txt

@@ -1,2 +1,3 @@
 add_subdirectory(Handshake)
 add_subdirectory(HW)
+add_subdirectory(Synth)