1ABC(1)                           User Commands                          ABC(1)
2
3
4

NAME

6       abc - sequential logic synthesis and formal verification
7

SYNOPSIS

9       abc [OPTIONS] FILE
10

DESCRIPTION

12       ABC  is a growing software system for synthesis and verification of bi‐
13       nary sequential logic circuits appearing in  synchronous  hardware  de‐
14       signs.   ABC combines scalable logic optimization based on And-Inverter
15       Graphs (AIGs), optimal-delay DAG-based technology mapping  for  look-up
16       tables  and  standard  cells,  and innovative algorithms for sequential
17       synthesis and verification.
18
19       ABC provides an experimental implementation of these algorithms  and  a
20       programming  environment for building similar applications.  Future de‐
21       velopment will focus on improving the algorithms and making most of the
22       packages  stand-alone.   This  will allow the user to customize ABC for
23       their needs as if it were a toolbox rather than a complete tool.
24

OPTIONS

26       -c CMD Execute commands CMD.
27
28       -q CMD Execute commands CMD quietly.
29
30       -C CMD Execute commands CMD, then continue in interactive mode.
31
32       -Q CMD Execute commands CMD quietly, then continue in interactive mode.
33
34       -F SCRIPT
35              Execute commands from script file SCRIPT and echo commands.
36
37       -f SCRIPT
38              Execute commands from script file SCRIPT.
39
40       -h     Print command usage.
41
42       -o FILE
43              Store the result in FILE.
44
45       -s     Do not read any initialization file.
46
47       -t TYPE
48              Specify the input type, one of blif_mv, blif_mvs, blif, or none.
49              The default is blif_mv.
50
51       -T TYPE
52              Specify  the  output  type,  one  of blif_mv, blif_mvs, blif, or
53              none.  The default is blif_mv.
54
55       -x     Equivalent to -t none -T none.
56
57       -b     Run in bridge mode.
58

INTRODUCTION

60       Data structures and algorithms at the heart of a software system deter‐
61       mine  its  capabilities in processing data and its efficiency as a pro‐
62       gramming environment for building new applications.  Extensive  experi‐
63       ence  of  developing and using SIS, VIS, and MVSIS, makes it clear that
64       these systems do not provide a flexible programming environment to  im‐
65       plement  recent  innovations, such as integration of technology mapping
66       and retiming.  Specifically, the SIS environment is outdated and rather
67       inefficient  when  handling  large circuits.  VIS, designed as a formal
68       verification tool for multi-valued  specifications,  does  not  provide
69       enough  flexibility  for binary synthesis.  MVSIS was developed and ex‐
70       tensively used by us in the recent years for implementing new synthesis
71       algorithms  for both multi-valued and binary networks.  Finally, we be‐
72       came convinced that (a) the basic data structures and algorithms of MV‐
73       SIS  can be made considerably simpler and easier to use by assuming bi‐
74       nary networks, and (b) a central place in  the  new  system  should  be
75       given  to  a  new data structure, AIGs (multi-level logic networks com‐
76       posed of two-input ANDs and inverters), which promises improvements  in
77       quality and runtime of synthesis and verification.
78
79       This understanding motivates us to redevelop the core packages of MVSIS
80       resulting in a new programming environment named ABC.  As the name sug‐
81       gests,  the primary goal is to keep data structures simple and flexible
82       for a wide range of applications.  The “philosophy of ABC” has  several
83       basic  premises.   One  of them is allowing for a variety of functional
84       representations, such as BDDs and SOPs,  to  solve  specialized  tasks,
85       while defaulting to AIGs for the mainstream network manipulation.  Rep‐
86       resenting logic using AIGs leads to a remarkable uniformity in computa‐
87       tion  and  efficient interfacing with CNF-based SAT solvers for handing
88       Boolean reasoning problems.  Another fundamental premise of ABC is  the
89       synergy  between  synthesis  and verification using efficient SAT-based
90       Boolean reasoning on the AIG for combinational and  sequential  equiva‐
91       lence checking.
92
93       The  goal  of the ABC project is to provide a public-domain implementa‐
94       tion of the state-of-the-art combinational and sequential synthesis al‐
95       gorithms  and,  at the same time, create an open-source environment, in
96       which such applications can be developed  and  compared.   The  current
97       version  of  ABC  can optimize/map/retime industrial gate-level designs
98       with 100K gates and 10K  sequential  elements  for  optimal  delay  and
99       heuristically  minimized area in about one minute of CPU time on a mod‐
100       ern computer.  The runtime of the combinational synthesis, mapping, and
101       verification is typically faster.
102
103
104
105ABC                             1.01 (20220731)                         ABC(1)
Impressum