|
Jerry James |
575c8c7 |
.TH "ABC" "1" "@VERSION@" "ABC" "User Commands"
|
|
Jerry James |
575c8c7 |
.SH "NAME"
|
|
Jerry James |
575c8c7 |
abc \- sequential logic synthesis and formal verification
|
|
Jerry James |
575c8c7 |
.SH "SYNOPSIS"
|
|
Jerry James |
575c8c7 |
.B abc
|
|
Jerry James |
575c8c7 |
[\fIOPTIONS\fP] \fIFILE\fP
|
|
Jerry James |
575c8c7 |
.SH "DESCRIPTION"
|
|
Jerry James |
575c8c7 |
.PP
|
|
Jerry James |
575c8c7 |
ABC is a growing software system for synthesis and verification of binary
|
|
Jerry James |
575c8c7 |
sequential logic circuits appearing in synchronous hardware designs. ABC
|
|
Jerry James |
575c8c7 |
combines scalable logic optimization based on And-Inverter Graphs (AIGs),
|
|
Jerry James |
575c8c7 |
optimal-delay DAG-based technology mapping for look-up tables and standard
|
|
Jerry James |
575c8c7 |
cells, and innovative algorithms for sequential synthesis and verification.
|
|
Jerry James |
575c8c7 |
.PP
|
|
Jerry James |
575c8c7 |
ABC provides an experimental implementation of these algorithms and a
|
|
Jerry James |
575c8c7 |
programming environment for building similar applications. Future development
|
|
Jerry James |
575c8c7 |
will focus on improving the algorithms and making most of the packages
|
|
Jerry James |
575c8c7 |
stand-alone. This will allow the user to customize ABC for their needs as if
|
|
Jerry James |
575c8c7 |
it were a toolbox rather than a complete tool.
|
|
Jerry James |
575c8c7 |
.SH "OPTIONS"
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-c\fP \fICMD\fP
|
|
Jerry James |
575c8c7 |
Execute commands \fICMD\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-q\fP \fICMD\fP
|
|
Jerry James |
575c8c7 |
Execute commands \fICMD\fP quietly.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-C\fP \fICMD\fP
|
|
Jerry James |
575c8c7 |
Execute commands \fICMD\fP, then continue in interactive mode.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-F\fP \fISCRIPT\fP
|
|
Jerry James |
575c8c7 |
Execute commands from script file \fISCRIPT\fP and echo commands.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-f\fP \fISCRIPT\fP
|
|
Jerry James |
575c8c7 |
Execute commands from script file \fISCRIPT\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-h\fP
|
|
Jerry James |
575c8c7 |
Print command usage.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-o\fP \fIFILE\fP
|
|
Jerry James |
575c8c7 |
Store the result in \fIFILE\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-s\fP
|
|
Jerry James |
575c8c7 |
Do not read any initialization file.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-t\fP \fITYPE\fP
|
|
Jerry James |
575c8c7 |
Specify the input type, one of \fIblif_mv\fP, \fIblif_mvs\fP, \fIblif\fP, or
|
|
Jerry James |
575c8c7 |
\fInone\fP. The default is \fIblif_mv\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-T\fP \fITYPE\fP
|
|
Jerry James |
575c8c7 |
Specify the output type, one of \fIblif_mv\fP, \fIblif_mvs\fP, \fIblif\fP, or
|
|
Jerry James |
575c8c7 |
\fInone\fP. The default is \fIblif_mv\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-x\fP
|
|
Jerry James |
575c8c7 |
Equivalent to \fI-t none -T none\fP.
|
|
Jerry James |
575c8c7 |
.TP
|
|
Jerry James |
575c8c7 |
\fB\-b\fP
|
|
Jerry James |
575c8c7 |
Run in bridge mode.
|
|
Jerry James |
575c8c7 |
.SH "INTRODUCTION"
|
|
Jerry James |
575c8c7 |
.PP
|
|
Jerry James |
575c8c7 |
Data structures and algorithms at the heart of a software system determine its
|
|
Jerry James |
575c8c7 |
capabilities in processing data and its efficiency as a programming
|
|
Jerry James |
575c8c7 |
environment for building new applications. Extensive experience of developing
|
|
Jerry James |
575c8c7 |
and using SIS, VIS, and MVSIS, makes it clear that these systems do not
|
|
Jerry James |
575c8c7 |
provide a flexible programming environment to implement recent innovations,
|
|
Jerry James |
575c8c7 |
such as integration of technology mapping and retiming. Specifically, the SIS
|
|
Jerry James |
575c8c7 |
environment is outdated and rather inefficient when handling large circuits.
|
|
Jerry James |
575c8c7 |
VIS, designed as a formal verification tool for multi-valued specifications,
|
|
Jerry James |
575c8c7 |
does not provide enough flexibility for binary synthesis. MVSIS was developed
|
|
Jerry James |
575c8c7 |
and extensively used by us in the recent years for implementing new synthesis
|
|
Jerry James |
575c8c7 |
algorithms for both multi-valued and binary networks. Finally, we became
|
|
Jerry James |
575c8c7 |
convinced that (a) the basic data structures and algorithms of MVSIS can be
|
|
Jerry James |
575c8c7 |
made considerably simpler and easier to use by assuming binary networks, and
|
|
Jerry James |
575c8c7 |
(b) a central place in the new system should be given to a new data structure,
|
|
Jerry James |
575c8c7 |
AIGs (multi-level logic networks composed of two-input ANDs and inverters),
|
|
Jerry James |
575c8c7 |
which promises improvements in quality and runtime of synthesis and
|
|
Jerry James |
575c8c7 |
verification.
|
|
Jerry James |
575c8c7 |
.PP
|
|
Jerry James |
575c8c7 |
This understanding motivates us to redevelop the core packages of MVSIS
|
|
Jerry James |
575c8c7 |
resulting in a new programming environment named ABC. As the name suggests,
|
|
Jerry James |
575c8c7 |
the primary goal is to keep data structures simple and flexible for a wide
|
|
Jerry James |
575c8c7 |
range of applications. The “philosophy of ABC” has several basic premises.
|
|
Jerry James |
575c8c7 |
One of them is allowing for a variety of functional representations, such as
|
|
Jerry James |
575c8c7 |
BDDs and SOPs, to solve specialized tasks, while defaulting to AIGs for the
|
|
Jerry James |
575c8c7 |
mainstream network manipulation. Representing logic using AIGs leads to a
|
|
Jerry James |
575c8c7 |
remarkable uniformity in computation and efficient interfacing with CNF-based
|
|
Jerry James |
575c8c7 |
SAT solvers for handing Boolean reasoning problems. Another fundamental
|
|
Jerry James |
575c8c7 |
premise of ABC is the synergy between synthesis and verification using
|
|
Jerry James |
575c8c7 |
efficient SAT-based Boolean reasoning on the AIG for combinational and
|
|
Jerry James |
575c8c7 |
sequential equivalence checking.
|
|
Jerry James |
575c8c7 |
.PP
|
|
Jerry James |
575c8c7 |
The goal of the ABC project is to provide a public-domain implementation of
|
|
Jerry James |
575c8c7 |
the state-of-the-art combinational and sequential synthesis algorithms and, at
|
|
Jerry James |
575c8c7 |
the same time, create an open-source environment, in which such applications
|
|
Jerry James |
575c8c7 |
can be developed and compared. The current version of ABC can
|
|
Jerry James |
575c8c7 |
optimize/map/retime industrial gate-level designs with 100K gates and 10K
|
|
Jerry James |
575c8c7 |
sequential elements for optimal delay and heuristically minimized area in
|
|
Jerry James |
575c8c7 |
about one minute of CPU time on a modern computer. The runtime of the
|
|
Jerry James |
575c8c7 |
combinational synthesis, mapping, and verification is typically faster.
|