Parallel Breadth-first BDD Construction

		 Bwolen Yang and David R. O'Hallaron

Abstract: With the increasing complexity of protocol and circuit
designs, formal verification has become an important research area and
binary decision diagrams (BDDs) have been shown to be a powerful tool
in formal verification.  This paper presents a parallel algorithm for
BDD construction targeted at shared memory multiprocessors and
distributed shared memory systems. This algorithm focuses on improving
memory access locality through specialized memory managers and partial
breadth-first expansion, and on improving processor utilization
through dynamic load balancing. The results on a shared memory system
show speedups of over two on four processors and speedups of up to
four on eight processors.  The measured results clearly identify the
main source of bottlenecks and point out some interesting directions
for further improvements.


@inproceedings{ppopp97bdd,
title = "Parallel Breadth-First BDD Construction",
author = "B. Yang and D. O'Hallaron",
booktitle = "Proc. of the Sixth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)" ,
month = jun,
address = "Las Vegas, NV",
year = "1997"
}