Global rebuilding of OBDD´s avoiding memory requirement maxima

It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an output-efficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(|P||Q|) and requires O(|P|+|Q|) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDD´s in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate OBDD representations of a given circuit in the course of its symbolic simulation. Here, the algorithm is used dynamically, whenever the size of the manipulated OBDD´s becomes too large