Currently under development by Berkeley Logic Synthesis and Verification Group
What is in the current release?
What is not in the current release?
Standard cell mapping commands
ABC is a growing software system for synthesis and verification of binary sequential logic circuits appearing in synchronous hardware designs. ABC combines fast scalable logic optimization based on And-Inverter Graphs (AIG) with innovative algorithms for integrated sequential optimization and verification. ABC is meant to provide an experimental implementation of these algorithms and, at the same time, become a convenient programming environment for building similar applications in the future. The current experimental release of ABC is the first one in the line of several planned releases. It contains the basic data structures with limited synthesis and verification options. Future development will focus on advanced combinational and sequential transformations.
Data structures and algorithms at the heart of a software system determine its capabilities in processing data and its efficiency as a programming environment for building new applications. Extensive experience of developing and using SIS, VIS, and MVSIS, made it clear that none of these systems provides a flexible programming environment that is efficient enough to implement recent innovations, such as integrated sequential optimization. Specifically, the SIS environment is outdated and rather inefficient when handling large circuits. VIS, designed as a formal verification tool for multi-valued specifications, does not provide enough flexibility for binary synthesis. MVSIS was developed and extensively used by us in the recent years for implementing new synthesis algorithms for both multi-valued and binary networks. Finally, we became convinced that (a) the basic data structures and algorithms of MVSIS can be made considerably simpler and easier to use by assuming binary networks, and (b) a central place in the new system should be given to a new data structure, AIGs, which promises dramatic improvements in quality and runtime of synthesis and verification.
This understanding motivates us to redevelop the core packages of MVSIS resulting in a new programming environment named ABC. As the name suggests, the primary goal is to keep data structures simple and flexible for a wide range of applications. The “philosophy of ABC” has several basic premises. One of them is allowing a variety of functional representations, such as BDDs and SOPs, for solving specialized tasks, while defaulting to AIGs for the mainstream network manipulation. Representing logic using AIGs, multi-level networks composed of two-input AND gates and inverters, leads to a remarkable uniformity in computation and efficient interfacing with the SAT solver for handing Boolean reasoning problems. Another fundamental premise of ABC is the synergy between synthesis and verification achieved by recording synthesis operations using an AIG database and enabling efficient SAT-based verification relying on the advantageous properties of AIGs.
The current release is the first step of the three-step development process. The release contains the foundations of the framework and the basics of combinational synthesis. The next two steps are: (1) implementing high-quality yet fast and scalable combinational optimization based on Boolean decomposition, don’t-cares, and new ways of sharing logic using AIGs, and (2) developing a fully integrated sequential optimization flow, which performs the combinational optimization and technology mapping in a combined fashion while “optimizing across the latch boundary”. The results obtained by prototyping these algorithms in MVSIS confirm the practicality of the projected work. The ultimate goal is to provide a public-domain experimental implementation of the above algorithms and, at the same time, create an open-source environment, in which such applications could be easily developed and experimented with. The experimental implementation should be able to optimize/map/retime for optimal delay and heuristically minimized area, followed by unbounded sequential equivalence checking, industrial gate-level designs with 100K gates and 10K sequential elements in about one minute of CPU time on a modern computer. Far-fetched as this goal may sound today, we believe it will be achieved in the near future.
- Basic data structures to represent and manipulate combinational and sequential technology-independent networks in a variety of ways: as a netlist, as an AIG, as a logic network with nodes represented by SOPs (a SIS-style network), as a logic network with nodes represented by BDDs (a BDS-style network), as a technology mapped network, etc.
- Input file parsers for BLIF, BENCH (ISCAS) format, a limited subset of structural Verilog (needed to read IWLS 2005 benchmarks).
- Output file writers for BLIF, BENCH (ISCAS) format, CNF (for combinational miters), and mapped BLIF (.gate format).
- Procedures to perform various manipulations on logic networks: creating combinational and sequential miters (product machines), unrolling sequential circuits for a number of timeframes, performing fast structural hashing and balancing of AIGs, etc.
- A simple and fast logic synthesis engine, which performs partial collapsing and algebraic factoring of combinational networks (sequential networks are currently considered as combinational by cutting at the register boundary).
- Procedures to detect and accumulate structurally different representations of Boolean functions (FRAIG package).
- Technology mappers for variable-LUT-size FPGAs and standard cells, applicable to traditional logic networks and logic network with structural choices
- Advanced combinational equivalence checking using FRAIG package
- Simple bounded sequential equivalence checking, which unrolls sequential circuits for a given number of timeframes and performs combinational equivalence of the resulting combinational circuits
- Advanced combinational logic synthesis (extraction of shared logic, don’t-care based optimization, Boolean decomposition, etc)
- Sequential synthesis (retiming, integrated retiming and technology mapping, resynthesis using subsets of unreachable states, etc)
- Unbounded sequential equivalence checking, in particular, equivalence checking based on information about transformations performed during synthesis
The platform-independent source code can be downloaded and used without restrictions.
http://www-cad.eecs.berkeley.edu/~alanmi/abc/abc50729.tar.gz (1.9 Mb)
The archive contains the following files:
File name | File size | Operating system | Description |
abc.dsp | 27,936 | Windows | Visual Studio project file |
abc.dsw | 529 | Windows | Visual Studio project file |
abc.opt | 52,736 | Windows | Visual Studio project file |
abc.plg | 29,454 | Windows | Visual Studio project file |
abc.rc | 601 | Both | ABC resource file |
abc50729 | 4,564,222 | Linux | Binary |
abc50729.exe | 430,080 | Windows | Binary |
depends.sh | 217 | Linux | Dependency script (courtesy Satrajit Chatterjee) |
makefile | 1,235 | Linux | Make file (courtesy Satrajit Chatterjee) |
src | - | Both | Directory containing source code |
The code contained in directory src of the archive compiles on both Windows (with Microsoft Visual Studio 6.0 or higher) and Linux (with GCC). To compile on Windows (assuming that Visual Studio is installed), unzip the archive, double-click on abc.dsw, select Project -> Rebuild All. The binary named abc.exe will be created in directory _TEMP. To compile on Linux, unzip the archive and run make. The binary named abc will be created in the root directory. The pre-compiled Window and Linux binaries, abc50729.exe and abc50729, are included in the archive. To make use of standard aliases and settings, resource file abc.rc should be present in the working directory when running the program.
This section provided a short description of commands implemented in the current release.
Basic commands are similar to those implemented in SIS, VIS, and MVSIS.
alias – Creates association of a character or a short word with an available command. For example, once alias ps print_stats is entered on the command line, typing ps at the prompt invokes print_stats. A list of standard aliases is included in the distribution in file abc.rc. This file is automatically loaded when the program starts.
echo – Prints a message to the standard output. Used to add human-readable comments that are printed on the screen while executing script files. The message should be in quotes. For example, line echo “Synthesis” present in the script results in word Synthesis printed on the screen.
empty – Frees all networks currently stored in memory.
help – Prints the list of all currently implemented commands.
history – Prints the list of command lines entered by the user since the program is started.
ls – (Windows only.) Prints the list of files present in the current directory.
quit – Exits the program.
set – Sets a parameter on the command line.
source – Executes a script. For example, given a script file optimize.scr, the line source optimize.scr will execute the script. The line source –x optimize.scr will execute the script and echo each command on the screen.
time – Prints two time measurements: (a) the time the program spent computing since the last invocation of command time and (b) the time the program spent computing since it was started.
unalias – Removes an alias previously set by command alias.
undo – Sets the current network to the network saved before executing the last command, which changes networks. For example, command print_stats does not change the network. So running undo after print_stats will set the current network to be the one before the last command that has changed it. If the last such command before print_stats was map, the current network after undo will be as it was before mapping.
The FGPA mapping options are currently limited to variable-LUT-size mapping, in which LUT of each size is characterized by area and delay. The largest allowed size of a LUT is 6 inputs. The program maps the circuit to achieve optimal delay using classical algorithms for DAG-mapping, followed by a heuristic area recovery. The mapping performed is a generic LUT mapping that does not take into account specific FPGA architecture, which typically contains not only programmable LUTs but programmable macrocells as well. The macrocells may contain LUTs mixed with MUXes and other gates. Fine-tuning the mapping process for a specific architecture may significantly improve mapping quality. In the future, an improved version of the FPGA mapper may be developed, which takes into account the specific macrocell architecture.
fpga – Performs FPGA mapping using the currently selected LUT library for the current network. If the current network is an AIG or an AIG with choices, it is used for mapping as it is. If the current network is a logic network, before mapping this command performs structural hashing of the factored forms of the nodes (resulting in an AIG) followed by balancing (resulting in an AIG that is well-balanced for delay). Both balancing and mapping take into account the arrival times of primary inputs which can be represented in BLIF. Switch –a disables area recovery and outputs the network as it is after delay optimal mapping.
print_lut – Prints the currently selected LUT library. Each LUT size is represented by two numbers (area and delay). The default LUT library is the library of 5-input LUTs.
read_lut – Read a LUT library from the file and sets it to be the current LUT library. For a simple example on representing the LUT library, run print_lut. The print-out has the same format as the input file.
FRAIG is a software package that constructs And-Inverter Graphs (AIGs) for Boolean functions while enforcing functional uniqueness of each AIG node. In the resulting graph, no two nodes have the same Boolean function, or Boolean functions that are complements of each other. Externally, FRAIG package exposes APIs that are similar to those of a BDD package but internally it uses simulation and SAT. The word fraiging means constructing AIGs in the FRAIG package. The capability of FRAIG package to construct functionally reduced AIGs by far exceeds the capability of the BDD package to construct BDDs. This makes functionally-reduced AIGs very useful in a variety of applications in synthesis and verification, and ABC a system possessing unique characteristics not available in other tools. The commands in this section provide access to the FRAIG package included in the current release.
fraig – Transforms the current network into a functionally-reduced AIG. A variety of command line options available with this command allow for selecting the number of simulation patterns, the number of SAT solver backtracks, etc. Command line switch –r disables functional reduction. Switch –s prevents applying functional reduction to the nodes with sparse functions (the functions, whose simulation information is composed of all 0’s or all 1’s.) Switch –c toggles recording alternative logic structures while performing functional reduction.
fraig_trust – Assumes that the current network was derived by parsing a file, in which the choice nodes (the nodes representing structurally equivalent implementations of logic functions) were represented as (multi-input) OR-gates, while all other nodes are two-input AND-gated. Both ORs and ANDs can have complemented inputs. This command transforms the network satisfying the above restrictions into a functionally reduced AIG in the “trust mode” (syntactically), without invoking the FRAIG package.
fraig_store – Stores the current network as one “synthesis snapshot” in the internal AIG database to be restored and used for technology mapping later.
fraig_restore – Converts the currently stored AIG snapshots into a FRAIG and sets it to be the current network, to which technology mapping can now be applied. The AIG database is reset by calling this command.
fraig_clean – Resets the AIG database without restoring it.
fraig_sweep – Detects functionally equivalent nodes in a logic network. Unlike fraig, which transforms the network into a functionally reduced AIG, this command preserves the network structure and only merges the functionally equivalent nodes. This command can be applied to the mapped network. The resulting network is still mapped but reduced.
read – Parses an input file using one of the available file readers. The file extension is used to determine what file parser to invoke. The file extensions that are currently recognized are: .blif, .bench, .v.
read_bench – Parses the input file in BENCH (ISCAS) format.
read_blif – Parses the input file in BLIF.
read_pla – Not implemented in the current release.
read_verilog – Parses the input file in a subset of structural Verilog, which includes all the keywords and directives needed for reading IWLS 2005 benchmarks. The parser has several known problems, for example, it does not parse correctly T-latches that are present in some of the designs.
write_bench – Outputs the current network into a BENCH file.
write_blif – Outputs the current network into a BLIF file.
write_cnf – Outputs the current network into a CNF file, which can be used with a variety of SAT solvers. This command is only applicable to combinational miter circuits.
write_gate – If the current network is mapped using a standard cell library, outputs the current network into a BLIF file, compatible with SIS and other tools. (The same genlib library has to be selected in SIS before reading the generated file.) The current mapper does not map the registers. As a result, the mapped BLIF files generated for sequential circuits contain unmapped latches.
print_factor – Prints the factored forms of the nodes in the current network.
print_fanio – Prints the distribution of nodes by the number of fanins and fanouts.
print_io – Prints the lists of primary inputs (PI), primary outputs (POs), and latches of the network.
print_stats – Prints the statistics of the current networks. The statistics printed depend on the current network representation.
Standard cell mapping implemented in the current release has several important aspects. It is an optimal-delay DAG mapping based on k-feasible cuts, which is similar to the classical optimal-delay DAG mapping for LUT-based FPGAs. The currently implemented mapping algorithms are “gain-based”, that is, they find a mapping independent of the load-dependent part of the delay. This assumption allows for a simple efficient algorithm, which has a global view of delay. In the future, we plan to implement a load-dependent mapper by post-processing the output of the gain-based mapper.
attach – Assumes that the current network was mapped but the information about gate assignment and pin-to-input binding is lost. Attempts to attach the gates from the current library to the logic nodes in such a way that the functionality of the nodes is preserved. The result of this operation is not unique. The delay properties of the resulting network may be different from the original mapped network if the gates have different delay-parameters for the pins that correspond to symmetric variables of the gates. For example, if two pins of NAND2 have different delay-parameters, while the binding of pins to node inputs is selected arbitrarily, the delay properties will not be preserved.
map – Performs standard cell mapping of the current network using the current library. If the current network is an AIG or an AIG with choices, it is used for mapping as it is. If the current network is a logic network, before mapping this command performs structural hashing of the factored forms of the nodes (resulting in an AIG) followed by balancing (resulting in an AIG that is well-balanced for delay). Both balancing and mapping take into account the arrival times of primary inputs which can be represented in BLIF. Switch –a disables area recovery and outputs the network as it is after delay optimal mapping. Another useful command, fraig_sweep, is applied after mapping by default (use switch –s to disable) to merge functionally equivalent nodes leading to additional savings in area.
print_library – Prints the currently selected standard cell library.
read_library – Reads a standard cell library from a file in GENLIB format.
read_super – Reads a supergate library from a file using the supergate library format.
super – Generates supergates for the given standard cell library.
super2 – Generates input- and delay- limited combinations of two-input ANDs and inverters. The resulting combinations can be considered technology-independent supergates.
unmap – Erases the mapping of the current network by replacing each gate by a logic node with function equal to the function of the gate.
This section lists several basic synthesis commands implemented in the current release. The available synthesis flow is based on repeated application of selective collapsing and algebraic factoring. Currently a logic cone is selected (command renode) and refactored (command strash) while making no attempts to reduce the number of AIG nodes or factored-form literals. As a result, the synthesis flow is typically 20x faster but gives inferior quality, compared to script.rugged or script.algebraic in SIS and mvsis.rugged in MVSIS. The future releases will address this problem by developing more intelligent restructuring transformations.
Another observation related to synthesis as implemented in the current release, is the deviation from the classical approach implemented in SIS and MVSIS. In these tools the node boundaries are always kept while optimizing the individual nodes (SIS commands simplify and full_simplify) and while reshaping one boundary at a time (SIS commands eliminate and resub). In the new system, node boundaries are initially destroyed by structural hashing (command strash) and temporarily created (command renode). In a sense, command renode can be seen as a reverse of the SIS command eliminate because the logic network in ABC is by default completely eliminated while command renode creates node boundaries on demand.
strash – Transforms the current network into an AIG by one-level structural hashing. The resulting AIG is a logic network composed of two-input AND gates and inverters represented as complemented attributes on the edges. Structural hashing is purely combinational transformation, which does not modify the number and positions of registers.
balance – Assumes that the input is an AIG and creates an equivalent AIG having the minimum delay, measured using logic levels of two-input AND-gates. The inverters do not count towards the number of logic levels. The resulting AIG is derived by algebraic balancing of the multi-input AND-gates contained in the original AIG. The balancing is applied in the topological order and selects the minimum delay tree-decomposition of each multi-input AND-gate. Balancing takes into account the arrival times of primary inputs, which can be represented in BLIF.
renode – Assumes that the input is an AIG. Creates node boundaries in this AIG and collapses the intermediate logic to form larger nodes. After this command is applied, the node functions are represented using BDDs.
collapse – Recursively composes the fanin nodes into the fanout nodes, resulting in a network, in which each primary output and latch input is produced by a node, whose fanins are primary inputs and latch outputs. Collapsing is performed by building global BDD and is therefore limited to relatively small circuits. After this command is applied, the node functions are represented using BDDs.
cleanup – Removes the dangling nodes, that is, the logic nodes that do not fanout into primary outputs and latches.
bdd – If the nodes of the logic network are represented using SOPs, changes the node representation to BDDs.
sop – If the nodes of the logic network are represented using BDDs, changes the node representation to SOPs.
frames – Unrolls a sequential circuit for the given number of time-frames. Switch –i toggles initializing the timeframes using the reset values of the latches. If the initialized option is chosen, the resulting network is combinational. If the uninitialized option is chosen, the resulting network is a sequential circuit with the same latches and the combinational logic replaced by multiple copies of the original logic.
logic – Transforms the structural netlist (composed of nets, logic nodes, and registers) into a logic network (composed of logic nodes and registers). In this current version, this command should not be called by the user. It is called automatically by the system after reading a network from file. As a result, the user of the current release can only work with AIGs and other types of logic networks.
miter – Computes the miter of the two networks specified on the command line. If only one circuit is given, the miter of this network with the current network is computed. If no network is specified on the command line, creates the miter of the current network and its spec (the network, which was used as the starting point for synthesis). If the current network is sequential, computes the sequential miter (the produce machine). The miter has only one primary outputs, which is equal to 1 if and only if the behavior of the networks differs. The networks, for which the miter computation is called, should have the same number and ordering of PIs, POs, and latches. When sequential miter is computed, there is no restrictions on the number and ordering of latches in the networks.
sat – Assumes that the current network is a combination miter. Transforms the circuit into CNF and internally applies a recent version of MiniSat to solve this miter. Alternatively, the miter can be written out in CNF (command write_cnf) and solved by an external SAT solver.
sis – Invokes an external binary of SIS to execute a command or a script for the current ABC network.
mvsis – Invokes an external binary of MVSIS to execute a command or a script for the current ABC network.
Two equivalence checking options are currently implemented.
cec – Combinational equivalence checking compares the PI/PO behaviors of two networks. If latches are present, the networks are cut at the latch boundary, latch inputs are added to primary outputs, latch outputs to primary inputs, and the behavior is compared for the extended sets of PIs and POs. By default, a hybrid approach based on fraiging and SAT solving is used to solve the miter. Switch –s enables a SAT-only approach.
sec – Implements bounded sequential equivalence checking for two sequential networks. The product machine is unrolled for the given number of timeframes specified on the command line using switch –f, resulting in a combinational miter. By default, a hybrid approach based on fraiging and SAT solving is used to solve the miter. Switch –s enables a SAT-only approach.
Since this is the first release of a complex system, it is inevitable that the system has bugs and other unexpected “features”. It is highly recommended that verification commands are used as often as possible during synthesis. Thus, command cec without any arguments can be run between individual synthesis transformations. Each time this command is invoked, the current network is compared with its specification (derived from the initial file) and the result of comparison is reported to the user.
For stand-alone compilation, the current version of ABC includes the complete source code of the decision diagram package CUDD (by Fabio Somenzi) and C-language version of MiniSat (by Niklas Eén and Niklas Sörensson).
Webpage started July 29, 2005, by Alan Mishchenko.