Decision Diagrams: Where do we go?

Abstract

Binary Decision Diagrams (BDDs) are widely used in the area of verification, synthesis and testing. With increasing number of applications, inherent problems, in particular the memory explosion problem, have become more and more apparent. As a consequence, the development of alternative types of Decision Diagrams (DDs) and a re-investigation of the core algorithms for BDD manipulation as well can be observed.

Starting with a brief review on 12 years of DD history the talk will comment on the status quo of DD research, discuss open problems and point out directions of future research. In more detail, the following points will be addressed:

In general, BDD algorithms are well studied. New methods, e.g. MORE, combination of DFS and BFS, offer interesting possibilities. But especially in sequential verification, further studies are necessary to understand the full power of the approaches.

In addition, to overcome the memory explosion problem, word-level DDs should be considered. Here, manipulation methods are much less developed, it is not clear whether e.g. combinational verification, fsm traversal, model checking are going to work in a comparable way as in the bit-level case. Even basic algorithms are missing. First steps to close this gap are given.

Work in progress shows that algorithms merging BDD experience with word-level capabilities have the potential to successfully cope with increasing circuit sizes.

Relevant Papers