Exact BDD Minimization and Linear Transformations

Abstract

Binary Decision Diagrams (BDDs) are a powerful tool and are frequently used in many applications in VLSI CAD, like synthesis and verification. Unfortunately, BDDs are very sensitive to the variable ordering and their size often becomes infeasible.

A new exact algorithm for finding the optimal variable ordering for BDDs is presented. The algorithm makes use of a lower bound technique known from VLSI design. Up to now this technique has been used only for theoretical considerations and it is adapted here.

Recently, a new approach for BDD minimization based on Linear Transformations (LTs), i.e. a special type of spectral techniques, has been proposed. An exact algorithm to find an optimal LT for the variables of a Boolean function to minimize its corresponding BDD is presented. To prune the huge search space, techniques from algorithms for finding the optimal variable ordering are used.

Then LTs for larger functions are studied in more detail. While so far only experimental results are known, for a family of Boolean functions it is proven that by LTs an exponential blow-up of the BDD size can be avoided. Furthermore, a heuristic method is presented that allows to significantly reduce the BDD sizes.

By experiments we give a comparison to the state-of-the-art methods to demonstrate the advantages of the approaches.

Relevant Papers

(with Wolfgang G"unther): Linear Transformations and Exact Minimization of BDDs , in Great Lakes Symposium on VLSI (GLSV'98), Lafayette, 1998, pp. 325-330.

(with Wolfgang G"unther): BDD Minimization by Linear Transformations , Technical Report Nr. 104, University of Freiburg, 1998.

(with Nicole Drechsler and Wolfgang G"unther): Fast Exact Minimization of BDDs, Design Automation Conference (DAC'98), San Francisco. Postscript not available yet.