Space- and Time-Efficient BDD Construction via Working Set Control

Binary decision diagrams (BDDs) have been shown to be a powerful tool in formal verification. Efficient BDD construction techniques become more important as the complexity of protocol and circuit designs increases. This paper addresses this issue by introducing three techniques based on working set control. First, we introduce a novel BDD construction algorithm based on partial breadth-first expansion. This approach has the good memory locality of the breadth-first BDD construction while maintaining the low memoryoverheadof the depth-first approach. Second, we describe how memory management on a per-variable basis can improve spatial locality of BDD construction at all levels, including expansion, reduction, and rehashing. Finally, we introduce a memory compacting garbage collection algorithm to remove unreachable BDD nodes and minimize memory fragmentation. Experimental results show that when the applications fit

• Type: Conference
• Year: 1998
• Where: ASPDAC
• Authors: Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron
• Keywords: ASPDAC 1998, BDD Construction, BDD Construction Algorithm, BDD Construction Techniques, Hardware