DOCSEARCHbyAlgolia
Submit Docs

ABC: Sequential Logic Synthesis and Formal Verification

repository·master·Indexed 22 days ago

https://github.com/berkeley-abc/abc

A comprehensive system for logic optimization, technology mapping, and verification of digital circuits. ABC supports interactive and batch modes, providing tools for AIG rewriting and synthesis workflows. It can be used as a standalone binary or integrated as a static/shared library in C and C++, featuring specialized packages such as AIG, GIA, and MiniAIG for AIG construction and manipulation.

Tokens
14.6K
Snippets
62
Records
75
Agent score
76%

What's inside ABC

  1. Compile ABC as a binary or static library

    master

    To compile ABC for use as a standalone command-line tool or as a static library, use the make command with the following targets:

    • Standalone Binary: Run make to compile the executable.
    • Static Library: Run make libabc.a to generate the static library.

    When using ABC as a static library in your own application, you must call Abc_Start() to initialize the framework and Abc_Stop() to shut it down.

    # Compile as a binary
make

# Compile as a static library
make libabc.a

  2. Compile ABC as C or C++ with namespaces

    master

    ABC can be compiled using either a C or C++ compiler. You can also control whether the code uses namespaces by setting the CC and ABC_NAMESPACE variables.

    • C (Default): Ensure CC=gcc and ABC_NAMESPACE is not defined.
    • C++ (No Namespaces): Ensure CC=g++ and ABC_NAMESPACE is not defined.
    • C++ (With Namespaces): Set CC=g++ and define ABC_NAMESPACE using the OPTFLAGS variable (e.g., -DABC_NAMESPACE=xxx).
    # Example: Compiling as C++ with a custom namespace 'my_abc'
make CC=g++ OPTFLAGS="-DABC_NAMESPACE=my_abc"

  4. Understand the placement package API structure

    master

    The placement package is organized into two main header files defining different levels of access:

    • place_base.h: Contains the basic data structures and the "external" API intended for general use.
    • place_gordian.h: Contains the "internal" API and specific configuration options.

  5. Manage the ABC Frame

    master

    The Abc_Frame_t object (the 'Frame') acts as the central container for all data during an ABC session, including networks, libraries, flags, and verification results. Most high-level operations involve reading from or writing to a Frame.

    Network and GIA Management

    • Abc_FrameReadNtk(Abc_Frame_t *p): Reads the current network (Abc_Ntk_t).
    • Abc_FrameReadGia(Abc_Frame_t *p): Reads the current GIA (Gate-level Integrated AIG) manager (Gia_Man_t).
    • Abc_FrameUpdateGia(Abc_Frame_t *p, Gia_Man_t *pNew): Updates the current GIA with a new manager.
    • Abc_FrameSetCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet): Sets the active network in the frame.

    Global Frame Access

    ABC provides mechanisms to access a global frame context:

    • Abc_FrameSetGlobalFrame(Abc_Frame_t *p): Sets the current frame as the global frame.
    • Abc_FrameGetGlobalFrame(): Retrieves the current global frame.
    • Abc_FrameReadGlobalFrame(): Reads the global frame.
    // Example: Accessing the global frame and reading the network
Abc_Frame_t *pFrame = Abc_FrameReadGlobalFrame();
if (pFrame) {
    Abc_Ntk_t *pNet = Abc_FrameReadNtk(pFrame);
    // Use the network...
}

  6. Manage ABC network state with undo and recall

    master

    ABC allows you to navigate through previous states of the logic network using undo and recall commands. This is useful when performing iterative synthesis or verification steps.

    • undo: Sets the current network to the one from the immediately preceding step.
    • recall [-h] <num>: Sets the current network to a specific previous step level.
      • <num>: The level to return to.
      • Note: The number of steps available for recall is determined by the savesteps parameter (set via set savesteps <num>).
    • empty [-h]: Removes all currently stored networks and restarts the frame.

    If no network is currently loaded, these commands will report an empty network error.

    # Undo the last operation
abc> undo

# Recall to a specific step (e.g., step 5)
abc> recall 5

# Clear all networks to start fresh
abc> empty

  7. How the ABC plugin interface works

    master

    The ABC plugin system for external binaries relies on a file-based interface. When a command is executed via the plugin interface, the following lifecycle occurs:

    1. Input/Output Generation: ABC generates two temporary files: an .aig file for the input (containing the current network) and an .out file for the output.
    2. Command Execution: ABC invokes the external binary with the following command structure: <binary_name> -abc -input=<input_file> -output=<output_file> <original_args>
    3. Data Extraction: After the binary completes, ABC reads the <output_file> to extract results. The output file must contain objects in the format <object name>: <object data> (e.g., result: proved).

    Supported Output Objects:

    • result:: Can be proved, failed, undetermined, or error.
    • counter-example:: A binary representation of the counter-example.
    • proof-invariant:: A text-encoded single-output AIG.
    • bug-free-depth:: An integer representing the depth checked.
    • abstraction:: A binary representation of the abstraction.
    • aig:: A binary representation of an AIG to be loaded into the current session.

  8. External binary command prefix and listing

    master

    External binaries integrated via the plugin system follow specific conventions for command discovery:

    • Command Prefix: Plugin-provided commands are identified by a leading comma (,).
    • Listing Commands: To discover available commands from a binary, call it with the -list-commands flag.

    Example Command Line Construction: If an external tool bip is used, a command might look like:

    bip -input=tmp.aig -output=tmp.out ,pdr -check -prop=5

  9. Install and compile zlib

    master

    To compile the zlib library and run the test suite on most Unix-like systems, use the following sequence of commands:

    1. Run the configuration script.
    2. Build and run the test program to ensure the library is working correctly.
    3. Install the library to the system.

    For Windows, use the specific makefiles located in win32/ or contrib/vstudio/. For VMS, use make_vms.com.

    ./configure
make test
make install

  10. Build the MiniSat solver (core or simp)

    master

    To build a release version of the solver (without assertions and statically linked), you must first set the MROOT environment variable to the directory containing the minisat source. Then, navigate to either the core or simp directory and run gmake rs. Finally, copy the resulting binary to your desired installation directory.

    Note: The simp directory contains an extended solver with simplification capabilities, while core contains the base version.

    export MROOT=<minisat-dir>
cd { core | simp }
gmake rs
cp minisat_static <install-dir>/minisat

  11. Requirements for the GORDIAN-like placement package

    master

    To use the GORDIAN-like placement package, you need an i386 Linux system (other systems may work with modifications) and a standard ANSI C development platform.

    Optional dependencies:

    • hMetis partitioner: Required for certain features. Place libhmetis.a and libhtmetis.h in the package directory. If not available, define NO_HMETIS in place_gordian.h.
    • Java SDK: Required if you wish to compile BookshelfView.
    • Perl: Required if you want to use additional script utilities.

  12. Use the Espresso CLI

    master

    Espresso is a command-line tool for logic synthesis and minimization. It operates on PLA (Programmable Logic Array) files and supports various subcommands for different logic operations like minimization, expansion, and reduction.

    Basic Usage

    espresso [options] [file]

    If no file is provided, it reads from stdin. If a file is provided, it reads the PLA data from that file.

    Common Options

    • -D[cmd]: Execute a specific subcommand (e.g., -Despresso, -Dsimplify, -Dexpand).
    • -o[type]: Select the output format. Supported types include f, fd, fr, fdr, pleasure, eqntott, kiss, and cons.
    • -e[opt]: Select specific Espresso optimization options such as fast, ness, nirr, unwrap, onset, pos, strong, eat, eatdots, kiss, or random.
    • -r[range]: Select a range for specific subcommands (e.g., d1merge, minterms, opoall) using the format first-last (e.g., -r0-10).
    • -s: Provide a short execution summary.
    • -t: Provide a detailed execution trace.
    • -x: Suppress printing of the solution.
    • -v[type]: Enable verbose debugging with specific types.
    • -Sn: Select a strategy for specific subcommands (e.g., opo, opoall, pair, pairall, so_espresso, so_both).

    Legacy Support

    The CLI also supports older flag styles:

    • -do [cmd] (equivalent to -D[cmd])
    • -out [type] (equivalent to -o[type])
    • -f, -fr, or -fdr to specify input types.
    espresso -Despresso input.pla
espresso -Dsimplify -o kiss input.pla
espresso -Dminterms -r0-5 input.pla