Binary Decision Diagrams (BDDs) are a data structure frequentlynused to represent complex Boolean functions in formal verificationnalgorithms. An efficient heuristic algorithm for dynamically reducingnthe size of large reduced ordered BDDs by optimally reordering smallnwindows of consecutive variables is presented. The algorithms have beennfully integrated into the Berkeley and Carnegie Mellon BDD packages innsuch a way that the current variable order dynamically changes and isncompletely transparent to the user. Dynamic reordering significantlynreduces the memory required for BDD-based verification algorithms, thusnpermitting the verification of significantly more complex systems thannwas previously possible. The algorithms exhibit a smooth tradeoffnbetween CPU time and reduction in BDD size for almost all BDDs tested
展开▼
