Randal E. Bryant
Skip Abstract Section
Abstract
Ordered Binary-Decision Diagrams (OBDDs) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and equivalence straightforward. A number of operations on Boolean functions can be implemented as graph algorithms on OBDD data structures. Using OBDDs, a wide variety of problems can be solved through symbolic analysis. First, the possible variations in system parameters and operating conditions are encoded with Boolean variables. Then the system is evaluated for all variations by a sequence of OBDD operations. Researchers have thus solved a number of problems in digital-system design, finite-state system analysis, artificial intelligence, and mathematical logic. This paper describes the OBDD data structure and surveys a number of applications that have been solved by OBDD-based symbolic analysis.
- S. B. 1978. Binary decision diagrams. IEEE Trans. Comput. C-27, 6 (Aug.), 509 516.Google Scholar
- P., DEVADA8, S., AND GHOSH, A. 1991. Boolean satisfiability and equivalence checking using general binary decision diagrams. In The Internattonal Conference on Computer Design (Cambridge, Mass., Oct.). IEEE, New York, pp. 259-264. Google Scholar
- D. L., BRYANT, R. E., AND SEGER, C.-J. H. 1991. Formal hardware verification by symbolic trajectory evaluation. In Proceedings of the 28th ACM / IEEE Design Automatton Conference (San Francmco, June). ACM, New York, pp. 397-402. Google Scholar
- C. L. 1989. Ordered binary decision diagrams and circuit structure. In The International Conference on Computer Design (Cambridge, Mass., Oct.), IEEE, New York, pp. 392 395.Google Scholar
- M. W., AND CHANDRA, A.K. 1980. Equivalence of free Boolean graphs can be decided probabilistically in polynomial time. Inf. Process. Lett. 10, 2 (Mar.), 80-82.Google Scholar
- S., AND FISHER, A. L. 1989. Verifying pipelined hardware using symbolic logic simulation. In The International Conference on Computer Deszgn (Boston, Oct.). IEEE, New York, pp. 217 221.Google Scholar
- K. S., BRYANT, R. E., AND RUDELL, R. L. 1990. Efficient implementation of a BDD package. In Procee&ngs of the 27th ACM / IEEE Destgn Automation Conference (Orlando, June). ACM, New York, pp. 40-45. Google Scholar
- N, R. K., HACHTEL, G. D., McMULLEN, C. T., AND SANGIOVANNI-VINCENTELLI, A. L 1984. Logic Mzntmization Algorithms for VLSI Synthests. Kluwer Academic Publishers, Boston. Google Scholar
- F., POWNALL, P., AND HUM, P. 1984. Apphcations of testability analysis: From ATPG to critical path tracing. In The International Test Conference (Philadelphia, Oct.). IEEE, New York, pp. 705-712.Google Scholar
- F.M. 1990. Boolean Reasoning. Kluwer Academic Publishers, BostonGoogle Scholar
- R.E. 1991. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Coraput. 40, 2 (Feb.), 205-213. Google Scholar
- R.E. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35, 6 (Aug.), 677-691. Google Scholar
- J.R. 1991. Using BDDs to verify multipliers. In Proceedings of the 28th ACM / IEEE Design Automatlon Conference (San Franciscm June). ACM, New York, pp. 408-412. Google Scholar
- J. R., CLARKE, E. M., AND McMmLAN, K. 1990a. Symbolic model checking: 102~ states and beyond In The 5th Annual IEEE Symposium on Logic in Computer Science (Philadelphia, June) IEEE, New York, pp. 428 439Google Scholar
- J. R., CLARKE, E. M., DILL, D. L., AND McMILLAN, K. 1990b. Sequential circuit verification using symbolic model checking. In Proceedtngs of the 27th ACM / IEEE Design Automation Conference (Orlando, June) ACM, New York, pp. 46-51. Google Scholar
- R, W., AND SIMONI$, H. 1987. Embedding Boolean expressions into logic programming. J. Symb. Comput. 4, 2 (Oct.), 191-205. Google Scholar
- E., AND MAmN, M.A. 1977. An approach to unified methodology of combinational switching circuits. IEEE Trans. Comput. C-26, 8 (Aug.), 745 756.Google Scholar
- , ANn BRYANT, R. E. 1989. Test pattern generation for sequential MOS circuits by symbolic fault simulation. In Proceedings of the 26th ACM / IEEE Design Automation Conference (Las Vegas, June). ACM, New York, pp. 418-423. Google Scholar
- E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. 8, 2 (Apr.), 244-263. Google Scholar
- , O., MADRE, J.-C., AND BERTHET, C. 1990. Verifying temporal properties of sequential machines without building their state diagrams. In Computer~Aided Verification '90 (Rutgers, N.J., June), E. M. Clarke and R. P. Kurshan, Eds., American Mathematical Society, Providence, RI, pp. 75-84. Google Scholar
- , Y., ISHIURA, N., AND YAJIMA, S. 1991. Probabitistic CTSS: Analysis of timing error probability in asynchronous logic circuits. In Proceedings of the 28th ACM / IEEE Design Automation Conference (San Francisco, June). ACM, New York, pp. 650-655. Google Scholar
- R., FILKORN, T., AND TAUBNER, D. 1991. Generating BDDs for symbolic model checking in CCS. In CAV'91, Third International Conference in Computer Aided Verification (Aalborg, Denmark, Jul.), K. G. Larsen and A. Skou, Eds., Springer-Verlag, pp. 203-213. Google Scholar
- , T. 1991. A method for symbolic verification of synchronous circuits. In Computer Hardware Description Languages and their Applications (Marseilles, Apr.). Proceedings of IFIP WG 10.2, Tenth International Symposium Amsterdam, North-Holland, D. Borrione and R. Waxman, Eds., pp. 229-239.Google Scholar
- , S., HOPCROFT, J., AND SCHMIDT, E. M. 1978. The complexity of equivalence and containment for free single variable program schemes. In Automata, Languages and Programmlng. Lecture Notes in Computer Science, vol. 62, G. Goes, J. Hartmanis, Ausiello, and Boehm, Eds. Springer-Verlag, Berlin, pp. 227-240. Google Scholar
- , M., FUJISAWA, H., AND KAWATO, N. 1988. Evaluations and improvements of a Boolean comparison program based on binary decision diagrams. In The International Conference on Computer-Aided Destgn (Santa Clara. Calif., Nov.). 1EEE, New York, pp. 2 5.Google Scholar
- M., KAK~TDA, T., AND MATSUNAGA, Y. 1991. Redesign and automatic error correction of combinational circuits. In Logic and Architecture Synthesis: Proceedings of the IFIP TCIO / WGIO. 5 Workshop on Logic and Architecture Synthesis (Paris, May 1990), P. Michel and G. Saucier, Eds. Elsevier, Amsterdam, pp. 35~ ~go.Google Scholar
- M. R., AND JOHNSON, D.S. 1979. Computers and Intractability. W. H. Freeman and Company, New York.Google Scholar
- J., AND MEINEL, C. 1992. Efficient analysis and manipulation of OBDDs can be extended to read-once-only branching programs. Tech. Rep. 92-10, Universit~it Trier, Fachbereich IV--Mathematik/ Informatik, Trier, Germany.Google Scholar
- , J., AND BUSHNELl,, M.L. 1990. EST: The new frontier in automatic test-pattern generation. In Proceedzngs of the 27th ACM / IEEE Design Automation Conference (Orlando, June). ACM, New York, pp. 667-672. Google Scholar
- EONG, S.-W., PLESSIER, B., HACHTEL, G. D., AND SOMENZL F. 1991. Variable ordering and selection for FSM traversal. In The International Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 476-479.Google Scholar
- ARPLUS, K. 1989. Using if-then-else DAGs for multi-level logic minimization. In Advance Research in VLSI, C. Seitz, Ed. MIT Press, Cambridge, Mass., pp. 101-118. Google Scholar
- IMURA, S., AND CLARK, E. M. 1990. A parallel algorithm for constructing binary decision diagrams. In The International Conference on Computer Design (Boston, Oct.). IEEE, New York, pp. 220-223.Google Scholar
- E, C.Y. 1959. Representation of switching circuits by binary-decision programs. Bell System Tech. J. 38, 4(July), 985-999.Google Scholar
- LIN, B., TOUATI, H. J., AND NEWTON, A.R. 1990. Don't care minimization of multi-level sequential logic networks. In The Internatwnal Conference on Computer-Aided Destgn (Santa Clara, Calif., Nov.). IEEE, New York, pp. 4{4 417.Google Scholar
- MADRE, J. C., ANn BILLON, J. P. 1988. Proving circuit correctness using formal comparison between expected and extracted behaviour. In Proceedings of the 25th ACM / IEEE Design Automation Conference (Anaheim, June). ACM, New York, pp. 205-210. Google Scholar
- MADRE, J.-C., AND COUDERT, O. 1991. A logically complete reasoning maintenance system based on a logical constraint solver. In The 12th International Joint Conference on Artificial Intelligence (Sydney, Aug.), Morgan Kaufman, San Mateo, CA, pp. 294-299.Google Scholar
- MADRE, J.-C, COUDERT, O., AND BILLON, J.P. 1989. Automating the diagnosis and rectification of design errors with PRIAM. In The Internatwnal Conference on Computer-A~ded Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 30-33.Google Scholar
- MALIK, S., WANG, A., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. 1988. Logic verification using binary decision diagrams in a logic synthes~s environment. In The International Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 6-9.Google Scholar
- MCMmLAN, K. L. 1992. Symbolic model checking: An approach to the state explosion problem. PhD thesis, School of Computer Science, Carnegie-Mellon Univ.Google Scholar
- MEAD, C. A., AND CONWAY, L 1980. Introduction to VLSI Systems. Addison-Wesley, Reading, Mass. Google Scholar
- vEINEL, C. 1990. Modi/ied Branching Programs and their Computational Power. Lecture Notes in Computer Science, vol. 370, G. Goos and J. Hartmanis, Eds. Springer-Verlag, Berlin. Google Scholar
- MINATO, S., ISHIURA, N., AND YAJIMA, S. 1990. Shared binary decision diagram with attributed edges for efficient Boolean function manipulation. In Proceedings of the 27th ACM / IEEE Design Automation Conference (Orlando, June). ACM, New York, pp. 52-57. Google Scholar
- OCHI, H., ISHIURA, N., AND YAJIMA, S. 1991. Breadth-first manipulation of SBDD of function for vector processing. In Proceedings of the 28th ACM / IEEE Design Automation Conference (San Francisco, June). ACM, New York, pp. 413-416. Google Scholar
- REEVES, D. S., AND IRWIN, M.J. 1987. Fast methods for switch-level verification of MOS circuits. IEEE Trans. CAD / IC CAD-G, 5 (Sept.), 766-779.Google Scholar
- SATO, H., YASUE, Y., MA?SUNAGA, Y., AND FUJITA. M 1990. Boolean resubstitution with permissible functions and binary decision diagrams. In Proceedings of the 27th ACM / IEEE Design Automation Conference (Orlando, June). ACM, New York. pp. 284-289. Google Scholar
- SELLERS, F. F., HSIAO, M. Y., AND BEARNSON, C. L. 1968. Analyzing errors with the Boolean difference. IEEE Trans. Comput. C-17, 7(July), 676 683.Google Scholar
- SRINIVASAN, A., KAM, T., MALIK, S., AND BRAYTON, R.K. 1990. Algorithms for discrete function manipulation. In The Internattonal Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 92-95.Google Scholar
- WEGENER, I. 1988. On the complexity of branching programs and decision trees for clique functions. J ACM 35, 2 (Apr.). 461-471 Google Scholar
Index Terms
- Symbolic Boolean manipulation with ordered binary-decision diagrams
Recommendations
Deciding Boolean Algebra with Presburger Arithmetic
We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines Boolean algebras of sets of uninterpreted elements (BA) and Presburger arithmetic operations (PA). BAPA can express the relationship between integer variables ...
Translation among CNFs, characteristic models and ordered binary decision diagrams
We consider translation among conjunctive normal forms (CNFs), characteristic models, and ordered binary decision diagrams (OBDDs) of Boolean functions. It is shown in this paper that Horn OBDDs can be translated into their Horn CNFs in polynomial time. ...
Comments