1ABC(1) User Commands ABC(1)
2
6 abc - sequential logic synthesis and formal verification
7
9 abc [OPTIONS] FILE
10
12 ABC is a growing software system for synthesis and verification of
13 binary sequential logic circuits appearing in synchronous hardware
14 designs. ABC combines scalable logic optimization based on And-
15 Inverter Graphs (AIGs), optimal-delay DAG-based technology mapping for
16 look-up tables and standard cells, and innovative algorithms for
17 sequential synthesis and verification.
18 ABC provides an experimental implementation of these algorithms and a
20 programming environment for building similar applications. Future
21 development will focus on improving the algorithms and making most of
22 the packages stand-alone. This will allow the user to customize ABC
23 for their needs as if it were a toolbox rather than a complete tool.
24
26 -c CMD Execute commands CMD.
27 -q CMD Execute commands CMD quietly.
29 -C CMD Execute commands CMD, then continue in interactive mode.
31 -Q CMD Execute commands CMD quietly, then continue in interactive mode.
33 -F SCRIPT
35 Execute commands from script file SCRIPT and echo commands.
36 -f SCRIPT
38 Execute commands from script file SCRIPT.
39 -h Print command usage.
41 -o FILE
43 Store the result in FILE.
44 -s Do not read any initialization file.
46 -t TYPE
48 Specify the input type, one of blif_mv, blif_mvs, blif, or none.
49 The default is blif_mv.
50 -T TYPE
52 Specify the output type, one of blif_mv, blif_mvs, blif, or
53 none. The default is blif_mv.
54 -x Equivalent to -t none -T none.
56 -b Run in bridge mode.
58
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
65 implement 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
70 extensively used by us in the recent years for implementing new synthe‐
71 sis algorithms for both multi-valued and binary networks. Finally, we
72 became convinced that (a) the basic data structures and algorithms of
73 MVSIS can be made considerably simpler and easier to use by assuming
74 binary 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 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 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
95 algorithms 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.
102ABC 1.01 (20200127) ABC(1)