Research related to ABC

ABC is a very popular open source Logic Synthesis project, some research implemented in ABC or related to ABC is recorded here.

This repo also helps people who want to read ABC code properly, research paper is a good start before accessing plain code.

Most of the paper referenced here can be found at Alan Mishchenko's publication page.

Another EPFL Isils group also has very high quality synthesis research, feel free to add anything interesting to the list.

General introduction

• ABC: An academic industrial-strength verification tool
  This introduction is a bit old but contains history of all Berkeley's tools and how ABC is started, it is written by Prof Robert Brayton.

• Quick Look under the Hood of ABC
  A brief but important manual helps understand basic network types and structures in ABC.

Command and Research Related

Structure & algorithm

Some structure concept such as K-feasible cuts, priority cuts, MFFC in ABC can be found in following research paper. - [CUDD package](https://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddIntro.html)
A manual helps get familiar with CUDD package. - Multi-valued Decision Diagram (MDDs) [Algorithms for discrete function manipulation](https://ieeexplore.ieee.org/document/129849) - [EXTRA library](https://people.eecs.berkeley.edu/~alanmi/research/extra/)
Should be used together with CUDD package. - [Liberty Reference Manual](https://people.eecs.berkeley.edu/~alanmi/publications/other/liberty07_03.pdf), there's probably a new version though, if anyone has a legal reference link, please update. - [Priority Cuts Definition](https://people.eecs.berkeley.edu/~alanmi/publications/2007/iccad07_map.pdf)
Priority cuts are cuts with cost function. - [Factor Cuts Definition](https://people.eecs.berkeley.edu/~alanmi/publications/2006/iccad06_cut.pdf)
There are two ways of generating cuts, [top-down or bottom-up](https://infoscience.epfl.ch/entities/publication/d9ae3daa-9ee9-4902-892d-ba7b3f241bfb). - [Cut Ranking and Pruning: Enabling A General And Efficient FPGA Mapping Solution](https://dl.acm.org/doi/pdf/10.1145/296399.296425) - [Fast Heuristic Minimization of Exclusive-Sums-of-Products](https://people.eecs.berkeley.edu/~alanmi/publications/2001/rm01_heu.pdf)
ESOP minimizer EXORCISM-4, compared with early EXMIN2/MINT/EXORCISM-2/EXORCISM3. - ISOP(Irredundant Sum-of-product computation)
Which is always computed by Minato-Morreale Algorithm, there is one Pseudo code in the [appendix part](https://cecs.uci.edu/~papers/compendium94-03/papers/1998/iccad98/pdffiles/02b_2.pdf), the truth table library in [Kitty](https://github.com/msoeken/kitty/blob/master/include/kitty/isop.hpp) also has an implementation.
Note BDD package seems to have internal interface. (Reference needed).

IO & Util Group

aigaug - Verilog-to-PyG A Framework for Graph Learning and Augmentation on RTL Designs - Logic-level augmentation. - Relevant repository.

&get & &put - ABC has ABC space and ABC9 space, example of using them interchangeably:
read_aiger i10.aig; strash; &get; &b; &st; &put; rewrite; refactor; ps
&r i10.aig; &st; &if -g; &put; balance; rewrite; ps
read_aiger i10.aig; strash; &get; &if -g; &ps

read_aiger - Local Two-Level And-Inverter Graph Minimization without Blowup
This one is referenced in ABC when constructing AIG. - AIGER 1.9 AND Beyond - The AIGER And-Inverter Graph (AIG) Format Version 20071012
This version is much more detailed than the latest one and illustrates the original AIG format and how to parse it. If you are working on a parser, read this carefully, I recommend reading the aiger parser in lorina, which is implemented in regular expression, in ABC, this is done by hard-core char by char shifting.
Prof Armin Biere's repo would help you do the transformation between aig and other format.

read_bench - Read a bench format file

read_blif - Berkeley Logic Interchange Format(BLIF) - BLIF-MV
BLIF-MV format is the extended BLIF format.

read_pla
PLA format is used as the input file format for Espresso, could find the manual here.

read_genlib & print_genlib - genlib format is SIS genlib format
*Note this is not an official source, it would be appreciated if anyone could provide an official source.

read_super - Concepts of supergates can be found in Reference0 and Reference1.

super - In ABC this command for constructing supergates only accepts a library in genlib format, if you are using a standard cell library, dump a genlib first.

testnpn - Fast Boolean Matching Based on NPN Classification - Fast Adjustable NPN Classification Using Generalized Symmetries

double - double can be used to increase the size of the current aig network, and functionally speaking, you could generate larger case more realistic than MtM benchmark. - Reference

&cec - Parallel Combinational Equivalence Checking
Note that exact -P and -S switch cannot be found here, if anyone has found the exact implementation in the paper, please update.

write_edgelist - Verilog-to-PyG A Framework for Graph Learning and Augmentation on RTL Designs - Graph Extraction.

write_bench - This command by default write out the LUT network, if you prefer the traditional gate representation, turn on -l.

Optimization Group

strash
Structural hashing - One-level strashing: Make sure nodes have different fanins(up to permutation). - Two-level strashing

bdd
Binary decision diagram.
*Note that Reduced Ordered Binary Decision Diagram(ROBDD) is canonical but even with structure hashing, AIG is not canonical, this is simple but important.

bidec
Bi-decomposition.
Reference: An Algorithm for Bi-Decomposition of Logic Functions (Compared to SIS, better delay result achieved.)

dsd - The Disjunctive Decomposition of Logic Functions
This command implements all the 4 cases in the paper above. - Other Disjoint Support Decomposition reference: - Minato-DeMicheli - Sasao-Matsuura - An approach to disjoint-support decomposition of logic functions
This implementation should be in EXTRA library.

dsec
Sequential Equivalence Checking. - Scalable and Scalably-Verifiable Sequential Synthesis

eliminate - Reference: "For example, the operation eliminate collapses a node into its fanouts if the worth of a node computed using this metric did not exceed a specified threshold."("this metric" stands for FFLC.)

&fx - Fast extract from The Testability-Preserving Concurrent Decomposition and Factorization of Boolean Expressions

ftune - FlowTune: End-to-end Automatic Logic Optimization Exploration via Domain-specific Multi-armed Bandit
Note that this command is not in the original ABC, the detail of the implementation is here.

fraig - FRAIGs: A Unifying Representation for Logic Synthesis and Verification
Construct aig and make sure it's semi-canonical, the concept semi-canonical can be compared with ROBDD, which is totally canonical.
Note that the MVSIS link in the paper is no longer available, unofficial source code could be retrieved from the *Traditional Logic synthesis tools** part below.

&iso - A Semi-Canonical Form for Sequential AIGs

orchestrate - DAG-aware Synthesis Orchestration - Greedy local optimization and domain specific optimization with orchestration of rewrite/refactor/resub.

profile - It profiles the gate structure in network, uses reverse engineer, helps when using transparent-boxing strategy and optimizing with don't care. - -a HA and FA: Structural reverse engineering of arithmetic circuits

rewrite/refactor/balance - DAG-Aware AIG Rewriting A Fresh Look at Combinational Logic Synthesis
*Note that based on this thread, you should consider using drw/drf. - For balance, check the original paper about bi-decomposition. - Note that in ABC, balance command have -d and -s option but implemented improperly which leads to same result, in mockturtle, the same algorithm skips these two options.

resub - Scalable Logic Synthesis using a Simple Circuit Structure
*Note that this resub is technology-independent, there is technology-dependent resub in reference, they have similar idea.

resub_unate - Fast resub based on detecting unate divisors - A Simulation-Guided Paradigm for Logic Synthesis and Verification

resub_core - Generic high-effort resub engine based on support selection
- Efficient Computation of ECO Patch Functions

twoexact - SAT-based exact synthesis with side-divisors - SAT Based Exact Synthesis using DAG Topology Families
*Note: The above three commands with commands such as runeco and &genrel can be found in this repo.

&reshape - Control Logic Restructuring for Area Optimization
*Note that although this command is already in ABC, no real implementation is available.

rr - Scalable Logic Synthesis using a Simple Circuit Structure
The concept of redundancy removal can be found here. The original redundancy removal could still be found in ABC source code but is not registered in the tool, so you can't use it directly, it is marked as absolete.
Note: *"... Therefore, dont-care-based two-level minimization performed in ... using ESPRESSO is not needed for AIG."

runeco - Efficient Computation of ECO Patch Functions

satclp - Progressive Generation of Canonical Irredundant Sums of Products Using a SAT Solver

&satlut - SAT-Based Area Recovery in Structural Technology Mapping

&transduction - Randomized Transduction for High-Effort Logic Synthesis

lutmin - Encoding of Boolean functions and its application to LUT cascade synthesis
The paper itself does not mention ABC but in this paper, reference links lutmin here.

lutpack - Fast Boolean Matching for LUT Structures - Boolean Factoring and Decomposition of Logic Networks

dchoice
Note: *"The command dchoice uses various methods for rewriting the AIG to minimize the number of AIG nodes while not increasing the number of its levels. In particular, dchoice strives for smaller delay by balancing, which decreases the number of AIG levels by decomposing wide-input AND gates in a balanced way." - Reference

indcut - Cut-Based Inductive Invariant Computation
You will see why one-hotness is collected in section 3.2, this technique is also used in command such as mfs.

if -S - Mapping into LUT Structures

if -g - Delay Optimization Using SOP Balancing
*Openroad flow use SOP balance in their script (Update 2024.1.2).
Optimize some aig structure rw/rf/b can't optimize.

if -y - Lazy Mans Logic Synthesis
Frequency based method to collect better pattern from design. Can even deal with patterns SOP-balance can not break.

if -u - Busy Mans Synthesis: Combinational Delay Optimization With SAT

Mapper Group

map
There are tons of ideas and tricks inside the mapper, this list will be extended. - Reducing Structural Bias in Technology Mapping - Technology Mapping with Boolean Matching, Supergates and Choices - Logic effort: Designing for speed on the back of an Envelope
Core theory, logic effort. - Gain-Based Technology Mapping for Discrete-Size Cell Libraries
Some gain-based method reference.
This reference is closely related to standard cell library mapping, which has discrete-size in each cell class (which means assumption of continuously sizeable cells does not hold). - Why delay estimation is logarithmic? High-Level Delay Estimation for Technology-Independent logic Equations

if - Combinational and Sequential Mapping with Priority Cuts

&sif - Mapping and Retiming Revisited

smap & sfpga - Integrating Logic Synthesis, Technology Mapping, and Retiming

atmap - A Design of Compressor Trees for LLM Module (IWLS 2025)

Other reference

• Recommend this slide about technology mapping by Prof Jie-Hong Roland Jiang.
• FlowMap: An Optimal Technology Mapping Algorithm for Delay Optimization in Lookup-Table Based FPGA Designs
  FlowMap
• Chortle: A Technology Mapping Program for Lookup Table-Based Field Programmable Gate Arrays
  Chortle
• Chortle-crf Fast Technology Table-Based Mapping for FPGAs
  Chortle-crf
• DAGON: Technology Binding and Local Optimization by DAG Matching
  The well known DAGON, you could probably see this in any reference(especially lecture slides/research paper etc.) online. Based on treeifying and dynamic programming.
• Delay-Optimal Technology Mapping by DAG Covering
  DAG mapper
  *Note: Faster than tree covering method in DAGON.
• Logic Decomposition during Technology Mapping
  Graph mapper
  Note: *"Using supergates and choices, the mapper outperforms both *Graph Map** and DAG mapper in delay and area and has a significantly shorter run-time."* - Reference.

Post-Mappinng Group

speedup - Global Delay Optimization using Structural Choices
*Note: ABC LUT library format also has examples in this paper. Since all optimization is on AIG as strash is performed after time tracing and critical node marking, so change these two part will help to apply the algorithm after standard cell mapping.

mfs & mfs2 & &mfs - Scalable Dont-Care-Based Logic Optimization and Resynthesis
Re-sub based resynthesis + don't care based resynthesis - Recommend using &mfs which is believed to be the newest and best version in ABC. (See note 5 on Page 12 of Reference.)

mfs3 - Versatile SAT-based Remapping for Standard Cells
Experiment is performed after amap and &nf -R 1000.
Note: mfs & mfs2 are for *LUT-based FPGAs** while mfs3 is for standard cells.
*Gain-based approach deals with delay information.

NPN

• Classifying n-Input Boolean Functions
  Very clear illustration of P/NPN class and examples are shown.

Verification Group

Property Checking & SEC (Sequential Equivalence Checking)

pdr - (2011) Efficient Implementation of Property Directed Reachability
Implements the Property Directed Reachability (PDR/IC3) algorithm, optimized for AIGs, for model checking safety properties.

bmc / &bmc / &bmcs / bmc2 / bmc3 - (1999) Symbolic Model Checking without BDDs
Performs Bounded Model Checking (BMC). ABC offers multiple implementations (bmc, &bmc, &bmcs, bmc2, bmc3) with varying features like static/dynamic unrolling, parallel solver support, etc.

ind - (2000) Checking Safety Properties Using Induction and a SAT-Solver
Performs K-step Induction to verify safety properties using a SAT solver.

int - (2003) Interpolation and SAT-based Model Checking
Uses SAT-based interpolation to perform model checking.

dprove - Enhancing and Integrating Model Checking Engines
Performs Sequential Equivalence Checking (SEC) on a sequential miter, combining techniques like abstraction refinement, speculative reduction.

reach / &reachm / &reachn / &reachp / &reachy - (1992) Symbolic model checking: 10^20 states and beyond (Foundational paper on BDD reachability)
Performs BDD-based reachability analysis for model checking. ABC provides multiple implementations (reach, &reachm, &reachn, &reachp, &reachy) using different BDD techniques and optimizations.

tempor - (2009) Enhanced Verification by Temporal Decomposition
Leverages temporal decomposition techniques to improve efficiency in sequential verification.

indcut - (2008) Cut-Based Inductive Invariant Computation
Uses cut-based methods to compute inductive invariants for model checking.

l2s - (2002) Liveness Checking as Safety Checking (Describes the underlying liveness-to-safety transformation)
Performs a liveness-to-safety transformation, converting the check of a liveness property into a safety property check.

kcs - (2012) A liveness checking algorithm that counts
Implements Claessen-Sorensson's k-Liveness algorithm for checking liveness properties.

LEC & Miter Solving & SAT Solving (Combinational Equivalence & SAT)

cec / &cec - (2006) Improvements to combinational equivalence checking (Discusses techniques used in CEC)
Performs Combinational Equivalence Checking (CEC), comparing two combinational circuits or a combinational miter.

&acec - Equivalence Checking using Gr obner Bases
Performs Combinational Equivalence Checking specialized for arithmetic circuits (e.g., multipliers).

iprove - (2006) Improvements to combinational equivalence checking
A newer engine for Combinational Equivalence Checking (CEC), integrating multiple techniques (rewriting, Fraiging, BDDs, SAT).

fraig / &fraig / dfraig / ifraig - (2003) FRAIGs: A Unifying Representation for Logic Synthesis and Verification
Performs combinational SAT sweeping to build Functionally Reduced And-Inverter Graphs (FRAIGs), a core technique for CEC.

sat / &sat - Chaff: Engineering an Efficient SAT Solver (Pioneering work in modern SAT solvers often used as baseline/inspiration)
Performs SAT solving to check the satisfiability of combinational circuit outputs, commonly used for miter solving. Often integrates solvers like MiniSat internally.

dsat / &dsat - An Extensible SAT-solver (MiniSat) (Describes MiniSat, often used by dsat)
Solves combinational miter SAT problems, often using an embedded MiniSat solver.

Delay target optimization

• Enabling Exact Delay Synthesis
  Personally really recommend this paper which combines timing information with supergates and optimizes searching using P classes with timing pattern.

Area target optimization

Traditional Logic synthesis tools

A brief historical view and corresponding introduction of UCB's synthesis and verification tool set:

• Old Logic synthesis tools
  Espresso, SIS, MVSIS are here.
  *Note: Some algorithm in ABC is directly from SIS and MVSIS.

• MIS MIS: A Multiple-Level Logic Optimization System

• SIS SIS: A System for Sequential Circuit Synthesis

• VIS(Verification Interacting with Synthesis)VIS : A System for Verification and Synthesis

• MVSIS MVSIS 2.0 Programmers Manual

  Benchmarks

  Here are some famous benchmarks from research/paper above.

• ESPRESSO benchmark

• IWLS 2022 Benchmarks

• IWLS 2005 Benchmarks

• IWLS 2024 Benchmarks

• EPFL combinational benchmark suite
  There's also a paper related to the benchmark.
  *Note that case hyp is quite big and skip it if necessary.

• Official AIG benchmarks can be found at here.

• ISCAS

• ITC99

• MCNC

• ISPD02 IBM Mixed-Size Placement Benchmarks

• ISPD98 Circuit Benchmark Suite - Reference

• ISPD04 IBM Standard Cell Benchmarks with Pads

• MPC Benchmark

• Crypto Benchmark

Other repo

Yosys and OpenRoad-flow-scripts are good place to find out discussion about ABC since original ABC repo's issues are not very active.

SAT solver

This [repo](https://www.cs.cmu.edu/~mheule/15816-f21/slides/practice.pdf) from CMU can give you a brief introduction on the DIMACS format and how to use SAT solver as an interface. I was trying to maintain a collection list of SAT solvers, but I have found that [PySAT](https://github.com/pysathq/pysat) seems to contain all the well-known SAT solvers. There's a detailed [introduction](https://people.eecs.berkeley.edu/~alanmi/courses/2007_290N/papers/intro_een_sat03.pdf) on MiniSAT.

Performance

• Yosys+ABC9 in FPGA is catching up with industry level performance. - Reference

• IWLS 2024: Yosys+ABC(Lazy Man Based): Insights from Basilisk: Are Open-Source EDA Tools Ready for a Multi-Million-Gate, Linux-Booting RV64 SoC Design?

TODO

Some of the implementation was originally been written into the traditional tools such as MVSIS or SIS.
It's better to check if ABC contains the following. - S&S-based and BDD-based resubstitution algorithms were implemented in the resynthesis package used to improve the quality of standard-cell technology mapping in MVSIS - Reference