ABC's rewrite-and-prove loop, and what it costs to depend on it

The equivalence gap ABC closes in a hardware flow

ABC is a system for sequential logic synthesis and formal verification, written in C and published from the berkeley-abc/abc repository. Its core job is narrow and specific: take a logic network, transform it into a different but logically identical network, and then prove the two are the same. That proof step is the `cec` command, and it is what makes ABC more than a rewriting toy. The audience is engineers who already know what a boolean network is: people checking an optimized gate-level netlist against its source form, researchers comparing rewriting strategies, and tool developers who want the rewriting and equivalence-checking code as a library rather than a binary. ABC is not a placement and routing tool, not a testbench simulator, and not a general-purpose SAT solver with a friendly front end. It reads logic networks in AIGER or BLIF format, reports on their structure, and answers the question of whether two versions of a network compute the same function.

The rewrite-and-compare loop behind cec

The verification loop is visible in the example command script the project ships. `r i10.aig` reads the network, `b` builds an AIG from it, `ps` prints the network statistics, `rw -l` and `rw -lz` rewrite it, and `cec` checks that the result is equivalent to what was read. Because the check is an equivalence proof rather than a functional simulation, the verdict covers the whole input space instead of a set of sampled vectors. The example output gives a concrete shape to what a rewrite buys. The network starts at 257 inputs and 224 outputs with 2396 AND nodes and 37 logic levels, and after the rewrite loop it reports 1851 AND nodes at 35 levels, followed by the line `Networks are equivalent.` The same run prints `Reading = 0.00 sec`, `Rewriting = 0.18 sec` and `Verification = 0.41 sec`. Those are timings from one illustrative run on one bundled file, not a throughput figure. The repository ships `i10.aig` at the top level, so the whole example is runnable from a fresh checkout without hunting for a benchmark.

Compiling the binary, the static library and the test suite

Building is a plain Make workflow. `make` produces the `abc` executable and `make libabc.a` produces the static library. The project also documents a CMake path that builds the executable and the regression tests, and those tests run in continuous integration on the supported configurations. Because the cyclic dependency check can stop a rebuild after a fresh checkout, the troubleshooting notes prescribe touching every file and rebuilding. Readline and pthreads are the two external dependencies that most often break a build, and each has a build flag to work around it. A shared library for plugin or language-binding use is built as position-independent code.

make
make libabc.a

The CMake route builds the executable and the regression tests in three commands.

cmake -S . -B build
cmake --build build
ctest --test-dir build --output-on-failure

If the build stops at the cyclic dependency check, run the following from the repository root and start again.

find . -type f -exec touch "{}" \;

A shared object, built as position-independent code, comes from a single extra flag.

make ABC_USE_PIC=1 libabc.so

Readline and pthread problems have their own escape hatches. `make ABC_USE_NO_READLINE=1` drops the readline dependency, and `make ABC_USE_NO_PTHREADS=1` builds without pthread support, which rules out concurrent embedding entirely. On systems where readline depends on curses, the curses library is named in `ABC_READLINE_LIBRARIES`.

One Abc_Frame_t per thread, and the commands that break the rule

Embedding is the part of ABC with the sharpest edges, and it is the part with the least slack. `Abc_Start()` and `Abc_Stop()` start and quit a single ABC session inside the calling application, and existing single-threaded programs built on those calls continue to work unchanged. For concurrent use the contract is stricter: each session gets its own `Abc_Frame_t` created with `Abc_FrameCreate()`, that frame must never be used concurrently by multiple threads, and it is released with `Abc_FrameDestroy()`. API calls made outside command execution that depend on the current frame are wrapped in `Abc_FrameEnter()` and `Abc_FrameLeave()`. Concurrency works on Linux and macOS and requires pthread support, so a build made with `ABC_USE_NO_PTHREADS=1` cannot use it. The documentation is explicit that some obsolete commands still use shared process state and are not safe to run in concurrent sessions, which is a genuine trap for a team that assumes every command in the interpreter is reentrant. The embedding examples live in `src/runabc.c`, and `src/demo.c` shows a standalone program doing DAG-aware AIG rewriting through the API.

gcc -Wall -O2 -Isrc -c src/runabc.c -o runabc.o
g++ -o runabc runabc.o libabc.a -lm -ldl -lreadline -lpthread

Running that binary with a thread count compares four concurrent sessions against a single-threaded baseline.

Interactive, batch and library sessions run the same script

The same command sequence can be issued three ways, and this is what makes ABC flexible enough for both a terminal and a CI job. Interactively, you type `r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec` at the `abc 01>` prompt. In batch mode the same string is passed as one `-c` argument, and ABC echoes it back as `ABC command line: "r i10.aig; ..."` before executing. The third route is the library, where `src/demo.c` performs DAG-aware AIG rewriting by calling the API directly instead of parsing a command string. The printed statistics and the equivalence verdict are identical across all three routes. Batch mode is the practical choice for automation because it needs no terminal, no readline and no interactive session, which also makes it the mode that behaves the same way in a container image.

./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"

The demo program built against the static library is compiled and run like this.

gcc -Wall -O2 -c src/demo.c -o demo.o
g++ -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread
./demo i10.aig

The demo and the batch run print the same numbers: 2396 AND nodes at 37 levels before rewriting, 1851 AND nodes at 35 levels after, and `Networks are equivalent.` at the end.

What the ABC documentation leaves undocumented

The project is candid about one thing: `ABC is always changing but the current snapshot is believed to be stable.` That sentence is the entire stability promise on offer, and it is a thin one. The repository has no GitHub releases, so there is no tagged version to pin against, no release notes to read, and no upgrade path to follow. The bug reporting section asks for an ABC version or Git commit, which for most users means a commit hash. The last push was on 2026-10-18 and the project is not archived. Several operational questions stay unanswered. There is no documented rollback procedure, no stated list of supported platforms beyond the build configurations that run in CI, and no explanation of what the custom licence in the LICENSE file grants or restricts. The regression suite is described as not exhaustive, so a green test run is a weak signal about a change. The named maintainer is Alan Mishchenko, and bug reports are directed to a mail address rather than an issue tracker.

The ZZ framework as an alternative route

The final remarks point to a second option: the ZZ framework by Niklas Een, hosted at the abc-zz repository. The two are not interchangeable in the same way as two flags. ABC is a self-contained program with a command interpreter plus a C library that other programs link. That difference matters for a team writing its own verification flow. The project offers a getting started tutorial contributed from EPFL for ABC and links for ZZ, but it does not give build steps for ZZ or compare the two, so choosing between them means reading both projects directly. ABC also publishes the exact list of information it wants in a bug report, which is a useful signal about how seriously the debugging process is taken.

Choosing the build shape and paying the upgrade cost

Three build shapes are supported and they carry different integration costs. The default `make` gives the `abc` executable, `make libabc.a` gives a static library to link into a host application, and `make ABC_USE_PIC=1 libabc.so` gives a shared object for a plugin or a language binding. A C or a C++ compiler is acceptable, and `make ABC_USE_NAMESPACE=xxx` compiles the C sources into a C++ namespace so the symbols do not clash inside a large host binary. The upgrade cost is the least documented part of the project. With no releases, an upgrade is a pull of the default branch, so anything you depend on can shift underneath you. The `Makefile` module list spans `src/opt/`, `src/sat/`, `src/map/`, `src/bool/` and more, so a single recompile brings in a large body of changed code at once, and the project's own advice to report a problem with the latest version assumes you are tracking that moving target. The licence is recorded as Other, a custom licence GitHub cannot classify, with the terms in the LICENSE file and the copyright notice in `copyright.txt`. Anyone planning to ship ABC inside a product has to read those two files directly rather than assume a permissive default.

Editorial conclusion

ABC suits engineers who already hold logic networks in AIGER or BLIF form and need an equivalence proof or a rewrite pass they can script or link, and it suits teams willing to follow the default branch themselves. It is a poor fit if you need tagged releases, a documented upgrade path or a licence readable at a glance, since the project publishes no GitHub releases and the terms sit in a custom LICENSE file. Before adopting, verify that your networks load with `r`, that the SAT and BMC engines you need appear in the `src/sat/` module list, and that none of the commands you plan to run is among the obsolete ones that still touch shared process state.

Frequently asked questions

Official sources

1. berkeley-abc/abc on GitHub
2. Issues
3. README