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. Recently, a new approach for BDD minimization based on linear transformations, i.e. a special type of spectral techniques, has been proposed. In this paper we study this minimization method in more detail. While so far only experimental results are known, we prove for a family of Boolean functions that by linear transformations an exponential blow up of the BDD size can be prevented. Furthermore, we present a heuristic method that allows to significantly reduce the BDD sizes. By experiments we give a comparison to the state-of-the-art method to demonstrate the advantages of our approach.