Efficient implementation of a BDD package

ABSTRACT

Efficient manipulation of Boolean functions is an important component of many computer-aided design tasks. This paper describes a package for manipulating Boolean functions based on the reduced, ordered, binary decision diagram (ROBDD) representation. The package is based on an efficient implementation of the if-then-else (ITE) operator. A hash table is used to maintain a strong canonical form in the ROBDD, and memory use is improved by merging the hash table and the ROBDD into a hybrid data structure. A memory function for the recursive ITE algorithm is implemented using a hash-based cache to decrease memory use. Memory function efficiency is improved by using rules that detect when equivalent functions are computed. The usefulness of the package is enhanced by an automatic and low-cost scheme for recycling memory. Experimental results are given to demonstrate why various implementation trade-offs were made. These results indicate that the package described here is significantly faster and more memory-efficient than other ROBDD implementations described in the literature.

REFERENCES

• 1: S. Malik, A, Wang, R. Braytori, and A, Sangiovanni- Vincentelli, "Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment," in Proc. Int. Conf. CAD (ICCAD-88), Nov. 1988, pp. 6-9.
• 2: M. Fujita, H. Fujisawa, and N. Kawato, "Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams," in Proc. Int. Conf. CAD (ICCAD- 88), Nov. 1988, pp. 2-5.
• 3: O. Coudert, C. Berthet, andJ. Madre, "Verification of Sequential Machines using Boolean Function Vectors," in IMEC-IFIP ira. Workshop on Applied Formal Methods for Correct VLS! Design, 1989.
• 4: S. Muroga , Y. Kambayashi , H. C. Lai , J. N. Culliney, The Transduction Method-Design of Logic Networks Based on Permissible Functions, IEEE Transactions on Computers, v.38 n.10, p.1404-1424, October 1989 [doi>10.1109/12.35836]
• 5: M. A. Breuer and A. D. Friedman, Diagnosis and Reliable Design of Digitial Systems. Computer Science Press, 1976.
• 6: P. C. McGeer , R. K. Brayton, Efficient algorithms for computing the longest viable path in a combinational network, Proceedings of the 26th ACM/IEEE conference on Design automation, p.561-567, June 25-28, 1989, Las Vegas, Nevada, United States [doi>10.1145/74382.74476]
• 7: K. Cho, Test Pattern Generation for Combinational and Sequential MOS Circuits by Symbolic Fault Siamlation. PhD thesis, Carnegie Mellon University, 1988.
• 8: M.R. Garey and D. S. Johnson, Computers and Inlractability. W. H. Freeman and Company, 1979.
• 9: Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
• 10: D. Bostick, G. D. Hachtcl, R. Jacoby, M. R, Lighmcr, E Moceyunas, C. R. Morrison, and D. Rav enscroft, "The Boulder Optimal Logic Design System," in Proc. Ira. Conf. CAD (ICCAD-87), Nov. 1987, pp. 62-65.
• 11: C. Y. Lee, "Representation of Switching Circuits by Binary- Decision Programs," Bell System Technical Journal, col. 38, pp. 985-999, July 1959.
• 12: Steven Fortune , John E. Hopcroft , Erik Meineche Schmidt, The Complexity of Equivalence and Containment for Free Single Variable Program Schemes, Proceedings of the Fifth Colloquium on Automata, Languages and Programming, p.227-240, July 17-21, 1978
• 13: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 14: D.S. Reeves and M. J. irwin, "Fast Methods for Switch-Level Verification of MOS Circuits," ~ Trans. Elec. Comp., col. CAD-6, pp. 766-779, Sep. 1987.
• 15: Kevin Karplus, REPRESENTING BOOLEAN FUNCTIONS WITH IF-THEN-ELSE DAGs, University of California at Santa Cruz, Santa Cruz, CA, 1988
• 16: S. B. Akers, "Functional Testing with Binary Decision Diagrams," in Eighth Annual Conference on Fault-Tolerant Computing, 1978, pp. 75-82.
• 17: Jean-Christophe Madre , Jean-Paul Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour, Proceedings of the 25th ACM/IEEE conference on Design automation, p.205-210, June 12-15, 1988, Atlantic City, New Jersey, United States
• 18: R. Lisanke, "Logic Synthesis Benchmarks," in Proc. Int. Workshop on Logic Synthesis (}WLS-89), May 1989.
• 19: Leonard Berman , Louise Trevillyan, A global approach to circuit size reduction, Proceedings of the fifth MIT conference on Advanced research in VLSI, p.203-214, January 1988, Cambridge, Massachusetts, United States

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN

  E. Data
  E.2 DATA STORAGE REPRESENTATIONS
      Subjects: Hash-table representations

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Design, Experimentation