IBDDs: an efficient functional representation for digital circuits

A central issue in the solution of many computer aided design problems is finding a concise representation for circuit designs and their functional specifications. Ordered binary decision diagrams (OBDDs) have recently emerged as a popular representation for various CAD applications such as design verification, synthesis, testing, modeling and simulation. Unfortunately, there is no efficient OBDD representation for many circuits, even in some cases for circuits which perform such apparently simple functions as multiplication. The authors present a new BDD representation scheme, called indexed BDDs (IBDDs), and show that it allows polynomial representations of functions which provably require exponential space using OBDDs. The key idea in IBDDs is to allow multiple occurrences of the input variables, subject to ordering constraints. The authors give an algorithm for verifying the equivalence of two IBDDs and a heuristic for constructing IBDDs for arbitrary combinational circuits