Sciweavers

ASPDAC
1998
ACM

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

13 years 7 months ago
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
Bwolen Yang, Yirng-An Chen, Randal E. Bryant, Davi
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1998
Where ASPDAC
Authors Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron
Comments (0)