Decision Diagrams: Where do we go?


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

MORE: Alternative Implementation of BDD-Packages by Multi-Operand Synthesis
A. Hett, R. Drechsler, B. Becker
IEEE European Design Automation Conference (EURODAC), Geneva, 1996

Fast and Efficient Construction of BDDs
A. Hett, R. Drechsler, B. Becker
IEEE European Design & Test Conference (ED&TC), Paris, 1997

Reordering Based Synthesis
A. Hett, R. Drechsler, B. Becker
3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design (Reed-Muller 97), Oxford, 1997

Polynomial Formal Verification of Multipliers
M. Keim, M. Martin, B. Becker, R. Drechsler, P. Molitor
IEEE VLSI Test Symposium (VTS), Monterey, 1997

Decision Diagrams in Synthesis - Algorithms, Applications and Extensions
B. Becker, R. Drechsler
IEEE VLSI Design Conference, Hyderabad, 1997

On the Computational Power of Bit-Level and Word-Level Decision Diagrams
B. Becker, R. Drechsler, R. Enders
Asia and South Pacific Design Automation Conference (ASP-DAC), Chiba, 1997

Overview of Decision Diagrams
R. Drechsler, B. Becker
IEE Proceedings, vol. 144, pp. 187-193, 1997

On the Expressive Power of OKFDDs
B. Becker, R. Drechsler, M. Theobald
Formal Methods in System Design: An International Journal (FORM), vol. 11 (1), pp. 5-21, 1997

The K*BMD: A Verification Data Structure
R. Drechsler, B. Becker, S. Ruppertz
IEEE Design & Test of Computers, pp. 51-59, April-June 1997
©2002-2018 U.C. Regents