Worst case examples for operations on OBDDs

Ordered BDDs (OBDDs) are representations of Boolean functions which have fo und a lot of applications in hardware and software verification, model chec king, and CAD. The reason is that OBDDs allow efficient algorithms for impo rtant operations like synthesis and equivalence check. Moreover, good varia ble orderings are constructed by heuristic algorithms like sifting. Here wo rst case examples for these operations and algorithms are presented. (C) 20 00 Elsevier Science B.V. All rights reserved.