Crate eqmap 

eqmap: FPGA LUT Remapping using E-Graphs

This Verilog-to-Verilog tool seeks to evaluate the use of logic rewriting and equality saturation for improving FPGA technology mapping.

The LUT representation can be found in the lut module, whereas a lot of the bit-twiddling of truth tables happens in rewrite. driver has all the code related to tooling and end-to-end integration.

eqmap_fpga is the main CLI tool, and you can see how it is used in some of the CI tests. Lastly, eqmap is bundled together with yosys in the eqmap script. This is the script that should be used to process your own verilog:

$ eqmap --help
Technology Mapping Optimization with E-Graphs

Usage: eqmap_fpga [OPTIONS] [INPUT] [OUTPUT]

Arguments:
  [INPUT]   Verilog file to read from (or use stdin)
  [OUTPUT]  Verilog file to output to (or use stdout)

Options:
      --report <REPORT>            If provided, output a JSON file with result data
  -a, --assert-sat                 Return an error if the graph does not reach saturation
  -f, --no-verify                  Do not verify the functionality of the output
  -c, --no-canonicalize            Do not canonicalize the input into LUTs
  -d, --decomp                     Find new decompositions at runtime
      --disassemble <DISASSEMBLE>  Comma separated list of cell types to decompose into
  -r, --no-retime                  Do not use register retiming
  -v, --verbose                    Print explanations (generates a proof and runs slower)
      --min-depth                  Extract for minimum circuit depth
  -k, --k <K>                      Max fan in size allowed for extracted LUTs [default: 6]
  -w, --reg-weight <REG_WEIGHT>    Ratio of register cost to LUT cost [default: 1]
  -t, --timeout <TIMEOUT>          Build/extraction timeout in seconds
  -s, --node-limit <NODE_LIMIT>    Maximum number of nodes in graph
  -n, --iter-limit <ITER_LIMIT>    Maximum number of rewrite iterations
  -h, --help                       Print help
  -V, --version                    Print version

Modules

analysis

The analysis stored with signals in the LUT network. In most respects, the analysis helps “type check” for any erroneous rewrite rules.

asic

Defines rewrite rules for ASIC cell mapping.

check

Implement useful utilities around model checking

cost

Simple cost functions that extracts LUTs with at most k fan-in.

driver

Common infrastructure to created command-line tools for logic synthesis using egg.

logic

Four-state logic

lut

Defines the grammar used to represent LUTs, gates, and principal inputs.

netlist

Support for nl-compiler

rewrite

Shannon decomposition, general cut-fusion, general cut-decomposition (using DSD), LUT symmetry, constant evaluation, and gate conversion rewrite rules.

verilog

Parses structural verilog and convert it into a SVModule struct.