A parallel algorithm for constructing binary decision diagrams

Abstract: "Ordered binary decision diagrams [1] are widely used for representing Boolean functions in various CAD applications. This paper gives a parallel algorithm for constructing such graphs and describes the performance of this algorithm on a 16 processor Encore Multimax. The execution statistics that we have obtained for a number of examples show that our algorithm achieves a high degree of parallelism. In paricular, with fifteen processors our algorithm is almost an order of magnitude faster on some examples than the program described in [2]. Moreover, on many examples it exhibits essentially linear speedup as the number of processors is increased.Our approach to binary decision diagrams is somewhat different from the one used in [1]. We view the binary decision diagram for an n-argument Boolean function as the minimal finite state automaton for the set of Boolean vectors of length n that satisfy f (i.e. the set of vectors in fΓäô(1)). Because the minimal finite automaton for a regular language is unique up to isomorphism, it is easy to argue that this representation provides a canonical form for Boolean functions. Boolean operations involving NOT, AND, OR, etc. are implemented by the standard constructions for complement, intersection, and union of the finite languages accepted by these automata.In general, each of these operations involves building a product automaton and then minimizing it. We discuss a parallel algorithm for computing the product of two automata and for minimizing the result. When we construct a binary decision graph, our algorithm follows the syntactic structure of the Boolean formula. First, the level of each Boolean operation is determined. Operations in the same level can be performed in parallel. If there are few operations at some level, then these operations are divided into a sequence of sub-operations that can be processed in parallel."