Resynth: circuit resynthesis by parts

Program Manual - BDS ver. 1.2.15 (January 2011)

Newly added (by Jan Schmidt) switches are indicated in bold.
       bds - BDD Based Logic Synthesis System

       bds [options] input-file

       bds -v

       BDS transfers a circuit (currently only combinational ckts) in BLIF
       format into a Boolean network. The Boolean network is then partitioned
       using SIS-eliminate-like procedure. The eliminate process is controlled
       by an eliminate gain threshold (EGT). Then sharing between different
       nodes are extracted. BDDs on each Boolean node are submitted to the
       decomposition engine to decompose. Phase assignment, homegeneous node
       collapse and final sharing extraction are done in the ftree processing
       phase. Finally the synthesis results are presented in equation, dot and
       BLIF format.

       BDS also provides a capability to verify the synthesized results by
       comparing the BDDs built on factoring trees with the original BDDs in
       the circuit.

       BDS generates a run directory with circuit name, date, time, machine
       name. All synthesis results and statistical information are stored in
       this directory. The synthesized results are in files, and All statistical information
       is in file If verbosity level 4 or greater is set, nine more
       files will also be generated. They are cktname.bds.*, cktname.sharing.*
       and cktname.collapse.*, they are mainly used for development purpose.

           input circuit in BLIF format. See FILES.

           Print BDS version and exit.

   BDD control
       -order initial_order
           The initial variable order of the BDD. The variable order in BLIF
           file is the default in BDS. You may need to use dfs to avoid huge
           initial BDD for some circuits, especially arithmetic circuits.

           Number of BDD nodes are calculated after variable reordering. This
           option should be used with caution. It may take long time on large
           test cases. Default is TRUE.

       -limitSize n
           The largest BDD size on which exact variable reordering can apply.
           This number is defined as # of variables times # of nodes on a BDD.
           Default is set to 200 which is a fairly small BDD.

       -miniMethod method
           Select the BDD minimization method. Currently restrict and
           licompaction are supported. Default is set to restrict.

           (TBD) Default is FALSE.

       -cache n
           Initial cache size for CUDD. Default is 10K.

       -maxmem n
           Memory size limit for CUDD in megabytes. Default is 10.

       -slots n
           (TBD) Default is CUDD_UNIQUE_SLOTS.

       -reordering method
           Select the BDD variable reordering method in CUDD. Currently are
           supported the following methods: none, random, bernard, pivot,
           sifting, converge, symm, tree, cotree, group, cogroup, win2, win3,
           win4, win2conv, win3conv, win4conv, annealing, genetic, linear,
           liconv, and exact. Default is set to none.

       -growth n 
           (TBD) Default is 20.

   Information output control
       -verb n
           verbosity level. There are three verbosity levels, 0, 1 and 4.

           At verbosity level 0, no additional trace information is output.

           Verbosity level 1 switches on summary statistics and dominator

           Verbosity level 4 brings detailed trace of attempted decomposition.
           Also, files with intermediate results are generated. See FILES.

   Algorithm control
       -ethred n
           Specify the eliminate gain threshold. Eliminate gain is calculated
           as number of BDD nodes on the merged node MINUS number of BDD nodes
           before the merge. Default is set to 0.

       -delta n
           Specify the disqualification threshold for X Hardcore. If one of
           the decomposed BDDs has the same support as the original one, and
           if the total number of nodes in the decomposed BDDs is greater at
           least by n, the decomposition is disqualified. The smaller n, the
           tighter is the requirement. Specifying n 1, 0, or even negative can
           usually prevent the X Hardcore algorithm from cycling (see KNOWN
           BUGS) at a small cost of decomposition efficiency. Default is set
           to INT_MAX, which disables this feature. Introduced in 1.2.02.

           By specifying this option, BDS will be forced to use local BDDs to
           do logic synthesis. Default is FALSE.

           By specifying this option, BDS will be forced to use global BDDs to
           do logic synthesis. Default is FALSE. If none of -useloc or -useglb
           is specified, BDS will pick a type of BDDs which is appropriate for
           better results.

       -globalLimit n
           Set the total number of BDD nodes. Since global BDD may offer a
           global minimization of the Boolean functions, BDS tries to build
           global BDD first. However, the tottal number of BDD nodes must be
           limited to prevent memory blow-up. Default is set to 20,000.

           Compared with traditional logic synthesis counterpart, SIS, BDS
           offers a unique way of eliminating nodes. By turnning this option
           on, all functional equivalent nodes are eliminated. However, global
           BDDs must be built first, which is impractical for most large
           circuits. Default is set to FALSE.

       -effort n
           how much effort BDS can afford. There are four level of effort, 1,
           2, 3 and 4. Currently, level 1 to 3 makes no difference. When
           effort is set to 4, BDDs are reordered using exact whenever they
           are smaller than size limitSize. Setting effort level to 4 does not
           mean the CPU time is much longer than other levels. Sometime the
           CPU time is even less than other lower levels. A good decomposition
           generates quasi-disjunctive BDDs(few variable overlap), therefore
           the number of follow-on decompositions is decreased. Default is set
           to 1. We recommend not to use this option.
           Do not perform Simple Dominator (algebraic) decomposition. Used for
           research purposes. As other algorithms require this decomposition
           already done, we do not recommend using this option. Default is to
           enable Simple Dominator decomposition. Introduced in 1.2.04.

           Do not perform Generalized Dominators decomposition. Used for
           research purposes. Default is to enable this decomposition.
           Introduced in 1.2.04.

           Do not perform Branch Hardcore decomposition. Used for research
           purposes. Default is to enable this decomposition. Introduced in

           Do not perform X Hardcore (XOR) decomposition. Used for research
           purposes. This option is equivalent to -xhardcore in bds-pga. Using
           this option is the crudest way to prevent BDS from endless XOR
           decomposition. There are circuits for which this decomposition
           method is crucial. On a small number of other circuits, disabling
           XOR decomposition slightly improves results. Default is to enable
           this decomposition. Introduced in 1.2.04.

           Do not perform Cofactor on Top decomposition. Used for research
           purposes. Default is to enable this decomposition. Introduced in

           Perfrom verification. Network partition and final synthesis results
           are verified. Default is FALSE.

   Output control
       -dir dir-name
           Force BDS to use dir-name as the output directory.  dir-name must
           not already exist. This is useful when running BDS from a script,
           as the default directory name (see FILES) is hard to predict.
           Introduced in 1.2.03.

           The Boolean network after eliminate is dumped into a file
  The file is in the current dir. Default is set to

           This option has no function. Default is set to FALSE.

           Write the factoring tree in text (EQN format). Total number of
           literals is counted in this file. Default is set to TRUE.

           Write the factoring tree in BLIF format. Default is TRUE.

           Write the factoring tree in dot format. Default is set to FALSE.

           Cut XORs, XNORs and MUX out from synthesized netlist. This
           preserves those cells which can be implemented as PTL manually. A
           file cktname.cutptl.blif will be generated. It just has AND/OR part
           of the final synthesis result.

   Input file
       Input file must be in Berkeley BLIF format. Both UNIX line ends (LF)
       and DOS line ends (CRLF) are tolerated (introduced in 1.2.07). Lines
       must not exceed MAXLENGTH-1 characters, and individual names must not
       exceed 1023 characters.The only directives recognized are: .model,
       .inputs, .outputs, .latch, .names, .exdc, .wire_load_slope, .end. No
       latches may pe present (combinational circuits only).

       Constant propagation should be performed on the circuit, e.g. by SIS
       sweep. As of 1.2.12, BDS does a rudimentary constant propagation itself
       and therefore the correctness of the result does not depend on the
       absence of internal constant generators.

   Output directory
       BDS creates a directory for all output files resulting from a run. The
       directory must not exist before executing BDS. Unless set by the -dir
       option, the directory name is cktname_MMM_dd_yyyy_hh_mm_ss_SSSS. where
       cktname is the circuit name taken over from the name of input file, MMM
       is month, dd is day in the month, yyyy is year, hh is hour, mm is
       minute, ss is second, and SSSS is host name. On systems where time does
       not work, MMM_dd_yyyy_hh_mm_ss is replaced by BDS's process number. On
       systems where uname does not work, _SSSS is absent.

   Output files
       All output files are created in the output directory. The final
       decomposed circuit is presented in files, and in equation, dot and BLIF
       formats respectively. The -dumpftree, -dumpfdot and -dumpfblif options
       were intended for selection of these files.

       All statistical information and run traces is in file If
       verbosity level 4 or greater is set, up to nine more files will also be
       generated. They are cktname.bds.*, cktname.sharing.*  and
       cktname.collapse.*, where * stands for eqn, dot, and blif. The
       selection of formats (equation, dot and BLIF) of those files also was
       intended to be controllable by the -dumpftree, -dumpfdot and -dumpfblif
       options. These file are mainly used for development purposes.

       Try the following commands, and compare with results of
       SIS(script.rugged), what do you think?

           bds -dumpfdot t481.blif

           bds -dumpfdot parity.blif

       BDS home page

           C. Yang, M. Ciesielski, V. Singhal: BDS: A BDD-Based Logic
           Optimization System.  In: Proceedings of the 37th Design Automation
           Conference (DAC'00), pp. 92-97.

           C. Yang, V. Singhal, M. Ciesielski: BDD decomposition for efficient
           logic synthesis. In: Proceedings of International Conference on
           Computer Design, 1999 (ICCD '99), pp. 626-631

       Algorithms and data structures
           C. Yang, M. Ciesielski: BDS: A BDD-Based Logic Optimization System.
           In: IEEE Trans. on CAD,vol. 21, no. 7 (July 2002), pp. 866-876.

       Performance on hard examples or Why is BDS Worth Maintaining
           P. Fiser, J. Schmidt: The Case for a Balanced Decomposition
           Process.  In: Proc. of 12th EUROMICRO Conference on Digital System
           Design., pp. 601-604.

       dot package

       CUDD package

       -   The decomposition may be trapped in a dead loop on some arithmetic
           circuit. A different initial variable order may walk around this
           bug. The bug is currently (1999) under investigation.

           As of 2011, this bug is still under investigation. For possible
           workarounds, refer to -xhc and -delta options.

       -   Binary options with default set to TRUE (-dumpftree, -dumpfblif)
           cannot be set to FALSE.

       -   The option format is neither POSIX nor GNU.

       -   Sweeping of constant nodes does not work. In sweep.c,
           bdsSweepConstant is empty and therefore BDS_SweepConstant must be

       -   The outputs in DOT and equation format have not been checked after
           extensive changes in BLIF export. They must be seen as unreliable
           until verified.

       Please send bug report to

       Congguang(Anda) Yang, with VLSI CAD Lab., Department of Electrical and
       Computer Engineering, University of Massachusetts Amherst.

1.2.15                             Jan 2011                             BDS(1)

BLIF file syntax

See here: Berkeley Logic Interchange Format (BLIF)