Also, very good are two pioneering papers by the "Father of Reduced Ordered Decision Diagrams", Randy Bryant.
1. R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677-691. Reprinted in M. Yoeli, Formal Verification of Hardware Design, IEEE Computer Society Press, 1990, pp. 253-267.
2. R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
Both of them are available from Randy Bryant's Home.
The following paper is of historical interest:
S.B.Akers, "Binary Decision Diagrams". IEEE Trans. on Computers, Vol. C-27, #6, pp.509-516, 1978.
The most decisive advances in the field have been made by Olivier Coudert and Jean Christophe Madre.
The first reader is O.Coudert, J.C.Madre. "Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions". Proc. of DAC '92, pp. 36-39.
Once it is clear how to encode and manipulate boolean cubes using two sets of binary variables (occurance variables and polarity variables), it is time to read the following papers:
O. Coudert, J. C. Madre, H. Fraisse, H. Touati, "Implicit Prime Cover Computation: An Overview", Proc. of SASIMI'93 (Synthesis And Simulation Meeting and Int'l Interchange), Nara, Japan, October 1993.
O. Coudert, J. C. Madre, H. Fraisse, "A New Viewpoint on Two-Level Logic Minimization", Proc. of 30th DAC, Dallas TX, USA, June 1993.
O. Coudert, "Two-Level Logic Minimization: An Overview", Integration. Vol. 17, No. 2, pp. 97-140, October 1994.
The last paper is quite comprehensive and looks like a text-book. The author reviews previous approaches to two-level minimization, including the classical Quine-McCluskey procedure and the more recent Brayton-McGeer-Sanghavi signature cube procedure. Next, he gives "the last word", a new completely implicit method by Coudert-Madre ("the last word" as of 1994, but I did not hear about any improvements since that time). All of the above papers and more, are available from the web link to Research publications of Synopsis researchers.
This link is a treasure trove. If we did not have any other imformation on implicit methods, only this link, we would still be able to understand the essential ideas.
Some helpful formulas and examples can be found in Chapter 10 "Implicit Formulation of Unate Covering" of the book: T.Villa, T.Kam, R.Brayton, A.Sangiovanni-Vincentelli. "Synthesis of Finite State Machines: Logic Optimization". Kluwer Academic Publishers, 1997. pp. 301-321.
There is another (reportedly less efficient) approach to two level minimization
by Gitanjali M. Swamy, Patrick McGeer and Robert K. Brayton. Their papers
and many other interesting publications are available from University of
California in Berkeley, Design Technology Warehouse, Research
Projects.
G. D. Hachtel, F. Somenzi. "Logic Synthesis and Verification Algorithms". Kluwer 1996. Section 7.10. "Symbolic FSM Traversal", pp. 308-312.
Herve J. Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, Alberto Sangiovannni-Vincentelli. "State Enumeration of Finite State Machines using BDDs". Proc. of ICCAD '90, pp. 130-133.
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley. "Efficient BDD Algorithms for FSM Synthesis and Verification". Proceedings of IEEE/ACM International Workshop on Logic Synthesis, Lake Tahoe, May 1995
Implicit techniques for state minimization through efficient solution
of binate covering problem are discussed in detail in the following publications:
.
T.Kam, T.Villa, R.Brayton, A.Sangiovanni-Vincentelli. "Synthesis
of Finite State Machines: Functional Optimization". Kluwer Academic Publishers,
1997.
T.Villa, T.Kam, R.Brayton, A.Sangiovanni-Vincentelli. "Synthesis of Finite State Machines: Logic Optimization". Kluwer Academic Publishers, 1997.
Y.T.Lai, M. Pedram, S.B.K.Vrudhula. "BDD-based decomposition of logic functions with application to FPGA synthesis". Proc. of DAC' 93. pp. 642-647.
Y.T.Lai, K.R.Pan, M. Pedram. "OBDD-based functional decomposition: Algorithms and implementation". IEEE Trans. on CAD, 15(8), pp.977-990, 1996.
In the following publications, available from Craig Files' Homepage, Multi-Valued Decision Diagrams are used to create a number of new methods for decomposition of multi-valued functions.
C. Files, R. Dreshler, M. Perkowski. "Functional Decomposition of MVL Functions using Multi-valued Decision Diagrams". IEEE International Symposium on Multi-Valued Logic, May 1997.
C. Files and M. Perkowski. "Multi-Valued Functional Decomposition as a Machine Learning Method". IEEE International Symposium on Multi-Valued Logic, May 1998.
Two innovative BDD-based methods for fast recursive computation of all single-output disjoint decompositions of binary functions (with don't cares - S. Minato, et al.) are presented in the following papers:
V. Bertacco, M. Damiani. "The Disjunctive Decomposition of Logic Functions". Proc. of ICCAD '97.
Shin-ichi Minato, Giovanni De Micheli. "Finding
All Simple Disjunctive Decompositions Using Irredundant
Sum-of-Products
Forms". ICCAD'98, pp. 111-117.
An interesting approach to bi-decomposition using cuts, reordering, and properties of complementary edges is presented in the following papers by VLSI design group at University of Massachusetts in Amherst:
C. Yang, V. Singhal, M. Ciesielski, "BDD Decomposition for Efficient Logic Synthesis". Intl. Conf. on Computer Design: VLSI in Computers and Processors, ICCD'99.
C. Yang, V. Singhal, M. Ciesielski, "Logic Optimization based on BDD Decomposition". Intl. Workshop on Logic Synthesis, IWLS'99.
These and some other research papers dealing with BDDs are available from the personal homepage of Maciej Ciesielski.
Formal
Verification Webpage at UCB
Ken McMillan's
Home Page at UCB
Model Checking at CMU
Hardware Verification Group at
Stanford
MONA Project Homepage, Denmark
Alan John Hu Homepage
at UBC, Canada
O. Coudert, J. C. Madre. "New Ideas for Solving Covering Problems". Proc. of 32nd DAC, San Francisco CA, June 1995.
T. Villa, T. Kam, R.K.Brayton, A.L.Sangiovanni-Vincentelli. "Explicit and Implicit Algorithms for Binate Covering Problems". IEEE Trans. on CAD. Vol. 16, No. 7, 1997, pp. 677-691.
M. Iwaihara and M. Hirofuji. "Implicit Representations of Graphs by OBDDs and Patricia BDDs". IEICE Trans. Fundamentals, Vol. E79-A, No. 7, pp. 1068-1078, July 1996.
A number of graph algorithms converted to implicit representation are discussed in these three papers:
E.M.Clarke, M. Fujita, P.C.McGeers, K.McMillan, J.C.Y.Yang. "Multi-terminal binary decision diagrams: An efficient data structure for matrix representation". IWLS'93. May 1993.
R.I.Bahar, E.A.Frohm, C.M.Gaona, G.D.Hachtel, E.Macii, A.Pardo, F. Somenzi. "Algebraic decision diagrams and their applications". Proc. of ICCAD. 1993. pp. 188-191.
F. Somenzi, G.D. Hachtel. "Symbolic Graph Algorithms". Workshop on Applications of Reed-Muller Expansion in Circuit Design (Reed-Muller '95). August 1995. Makuhari, Chiba, Japan, pp. 54-61.
An interesting paper presenting "classical" graph algorithms (max cliques, max independent set, min covering, etc.) in the context of Zero-Suppressed BDDs.
O.Coudert. "Solving graph optimization problems with ZBDDs". Proc. European Design and Test Conference, 1997.
S. Horeth, R. Drechsler. "Formal Verification of Word-Level Specifications". 1999 Design Automation and Test in Europe (DATE '99), March 9 - 12, Munich, Germany, pp. 52-58.
Note that some of the recent DAC, ICCAD, and DATE proceedings (including DAC '99!) do not require an IEEE Computer Society Digital Library access password, if you approach them through ACM:) Special thanks are to Special Interest Group on Design Automation, whose Proceedings Archives are open for download free of charge.
A valuable collection of papers dealing with various types, aspects, and applications of DDs can be found on the webpages of Dagstuhl Seminars "Computer Aided Design and Test". Year 1995 - Year 1997 - Year 1999.
The rational motivation, which I use to support my choice, is that BuDDy
Here are a couple of papers presenting the bdd package implemenation:
K.S.Brace, R.L.Rudell, R.Bryant. "Efficient implementation of a BDD package". Proc. of DAC 1990. pp.40-45.
M.Miller, R.Drechsler. "Implementing a Multi-Valued Decision Diagram Package". Proc. of Intl. Symp. on MV Logic. 1998.
S. Manne, D. Grunwald, F. Somenzi. "Remembrance of Things Past: Locality and Memory in BDDs". Proc. of DAC 1997.
Randy
Bryant
Rolf
Drechsler (publications)
Fabio Somenzi
Ken McMillan
Rajeev Ranjan
Adnan Aziz
Bill Lin
Applications
of Binary Decision Diagrams in Logic Synthesis, Verification, and Testing.
Invited presentation at the seminar in the University of Massachusetts,
Amherst, Friday, October 22, 1999.
Please comment on this page and email
links to relevant sources that are not mentioned here!