README.md 5.6 KB
Newer Older
1 2 3
[![.github/workflows/build-posix.yml](https://github.com/berkeley-abc/abc/actions/workflows/build-posix.yml/badge.svg)](https://github.com/berkeley-abc/abc/actions/workflows/build-posix.yml)
[![.github/workflows/build-windows.yml](https://github.com/berkeley-abc/abc/actions/workflows/build-windows.yml/badge.svg)](https://github.com/berkeley-abc/abc/actions/workflows/build-windows.yml)
[![.github/workflows/build-posix-cmake.yml](https://github.com/berkeley-abc/abc/actions/workflows/build-posix-cmake.yml/badge.svg)](https://github.com/berkeley-abc/abc/actions/workflows/build-posix-cmake.yml)
4

5 6 7 8 9 10 11
# ABC: System for Sequential Logic Synthesis and Formal Verification

ABC is always changing but the current snapshot is believed to be stable. 

## Compiling:

To compile ABC as a binary, download and unzip the code, then type `make`.
Alan Mishchenko committed
12
To compile ABC as a static library, type `make libabc.a`.
13 14 15 16 17 18 19 20 21

When ABC is used as a static library, two additional procedures, `Abc_Start()` 
and `Abc_Stop()`, are provided for starting and quitting the ABC framework in 
the calling application. A simple demo program (file src/demo.c) shows how to 
create a stand-alone program performing DAG-aware AIG rewriting, by calling 
APIs of ABC compiled as a static library.

To build the demo program

Alan Mishchenko committed
22
 * Copy demo.c and libabc.a to the working directory
23
 * Run `gcc -Wall -g -c demo.c -o demo.o`
24
 * Run `g++ -g -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread`
25 26 27

To run the demo program, give it a file with the logic network in AIGER or BLIF. For example:

28
    [...] ~/abc> demo i10.aig
29 30 31 32 33 34 35
    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
    Networks are equivalent.
    Reading =   0.00 sec   Rewriting =   0.18 sec   Verification =   0.41 sec

The same can be produced by running the binary in the command-line mode:

36
    [...] ~/abc> ./abc
37 38 39 40 41 42 43 44
    UC Berkeley, ABC 1.01 (compiled Oct  6 2012 19:05:18)
    abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec
    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
    Networks are equivalent.

or in the batch mode:

45
    [...] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
46 47 48 49 50 51 52 53 54 55 56 57 58 59
    ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec".
    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
    Networks are equivalent.

## Compiling as C or C++

The current version of ABC can be compiled with C compiler or C++ compiler.

 * To compile as C code (default): make sure that `CC=gcc` and `ABC_NAMESPACE` is not defined.
 * To compile as C++ code without namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is not defined.
 * To compile as C++ code with namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is set to
   the name of the requested namespace. For example, add `-DABC_NAMESPACE=xxx` to OPTFLAGS.

60 61 62 63 64 65 66
## Building a shared library

 * Compile the code as position-independent by adding `ABC_USE_PIC=1`.
 * Build the `libabc.so` target: 
 
     make ABC_USE_PIC=1 libabc.so

67 68 69
## Bug reporting:

Please try to reproduce all the reported bugs and unexpected features using the latest 
70
version of ABC available from https://github.com/berkeley-abc/abc
71 72 73

If the bug still persists, please provide the following information:    

Baruch Sterin committed
74
 1. ABC version (when it was downloaded from GitHub)
75 76 77 78 79 80 81 82 83 84 85
 1. Linux distribution and version (32-bit or 64-bit)
 1. The exact command-line and error message when trying to run the tool
 1. The output of the `ldd` command run on the exeutable (e.g. `ldd abc`).
 1. Versions of relevant tools or packages used.


## Troubleshooting:

 1. If compilation does not start because of the cyclic dependency check, 
try touching all files as follows: `find ./ -type f -exec touch "{}" \;`
 1. If compilation fails because readline is missing, install 'readline' library or
86
compile with `make ABC_USE_NO_READLINE=1`
87
 1. If compilation fails because pthreads are missing, install 'pthread' library or
88
compile with `make ABC_USE_NO_PTHREADS=1`
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
    * See http://sourceware.org/pthreads-win32/ for pthreads on Windows
    * Precompiled DLLs are available from ftp://sourceware.org/pub/pthreads-win32/dll-latest
 1. If compilation fails in file "src/base/main/libSupport.c", try the following:
    * Remove "src/base/main/libSupport.c" from "src/base/main/module.make"
    * Comment out calls to `Libs_Init()` and `Libs_End()` in "src/base/main/mainInit.c"
 1. On some systems, readline requires adding '-lcurses' to Makefile.

The following comment was added by Krish Sundaresan:

"I found that the code does compile correctly on Solaris if gcc is used (instead of 
g++ that I was using for some reason). Also readline which is not available by default 
on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package 
from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local 
include files for readline and LIBS to add the local libreadline.a. Perhaps you can 
add these steps in the readme to help folks compiling this on Solaris."

105 106 107
The following tutorial is kindly offered by Ana Petkovska from EPFL:
https://www.dropbox.com/s/qrl9svlf0ylxy8p/ABC_GettingStarted.pdf

108 109 110 111
## Final remarks:

Unfortunately, there is no comprehensive regression test. Good luck!                                

112
This system is maintained by Alan Mishchenko <alanmi@berkeley.edu>. Consider also 
Baruch Sterin committed
113
using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz (or https://github.com/berkeley-abc/abc-zz)