Boolean function manipulation on massively parallel computers

A new algorithm for implementing the basic operations on BDDs (binary decision diagrams) on a massively parallel computer is presented. Each node is associated with a processor, and nodes belonging to the same level are evaluated together. An implementation of the algorithm on a Connection Machine CM2 has been done, and the prototype is being tested on a set of benchmark applications. Experimental results, showing the time required to perform the apply operation on BDDs of growing size demonstrate the exactness of the complexity analysis and the effectiveness of the approach