Symbolic Boolean manipulation with ordered binary-decision diagrams
- 1 September 1992
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Computing Surveys
- Vol. 24 (3) , 293-318
- https://doi.org/10.1145/136035.136043
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.Keywords
This publication has 10 references indexed in Scilit:
- Verifying temporal properties of sequential machines without building their state diagramsPublished by American Mathematical Society (AMS) ,1991
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplicationIEEE Transactions on Computers, 1991
- Breadth-first manipulation of SBDD of Boolean functions for vector processingPublished by Association for Computing Machinery (ACM) ,1991
- On the complexity of branching programs and decision trees for clique functionsJournal of the ACM, 1988
- Embedding boolean expressions into logic programmingJournal of Symbolic Computation, 1987
- Fast Methods for Switch-Level Verification of MOS CircuitsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1987
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Analyzing Errors with the Boolean DifferenceIEEE Transactions on Computers, 1968
- Representation of Switching Circuits by Binary-Decision ProgramsBell System Technical Journal, 1959