OBDD minimization based on two-level representation of Boolean functions

In this paper, we analyze the basic properties of some Boolean function cla sses and propose a low complexity OBDD variable ordering algorithm, which i s exact (optimum) to some classes of functions and very effective to genera l two-revel form functions. We show that the class of series-parallel funct ions, which can be expressed by a factored form where each variable appears exactly once, can yield exact OBDD variable orderings in polynomial time. We also study the thin Boolean functions whose corresponding OBDDs can be r epresented by the form of thin OBDDs in which the number of nonterminal nod es is equal to the number of input variables. We show that a thin Boolean f unction always has an essential prime cube cover and the class of series-pa rallel functions is a proper subset of thin Boolean functions. We propose a heuristic viewing OBDDs as evaluation machines with function cube covers a s their inputs and apply a queuing principle in the algorithm design. Our h euristic, the augmented Dynamic Shortest Cube First algorithm, is proven to be optimum for the series-parallel functions and also be very effective fo r general two-level form functions. Experimental results on a large number of two-level form benchmark circuits show that the algorithm yields an OBDD total size reduction of over 51 percent with only 7 percent CPU time compa red to the well-known network-based Fan-in Heuristic implemented in the SIS package. Comparing to the known;exact results, ours is only 49 percent lar ger in size white only uses 0.001 percent CPU time.