Formal verification based on Boolean expression diagrams.

*(English)*Zbl 1266.68004
Electronic Notes in Theoretical Computer Science 56. Amsterdam: Elsevier; Lyngby: TU Denmark, Department of Information Technology (Diss. 2000). iv, 190 p., electronic only (2001).

Summary: This dissertation examines the use of a new data structure called Boolean Expression Diagrams (BEDs) in the area of formal verification. The recently developed data structure allows fast and efficient manipulation of Boolean formulae. Many problems in formal verification can be cast as problems on Boolean formulae. We chose a number of such problems and show how to solve them using BEDs.

Equivalence checking of combinational circuits is a formal verification problem which translates into tautology checking of Boolean formulae. Using BEDs we are able to preserve much of the structure of the circuits within the Boolean formulae. We show how to exploit the structural information in the verification process.

Sometimes combinational circuits are specified in a hierarchical or modular way. We present a method for verifying equivalence between two such circuits. The method builds on cut propagation. Assuming that the two circuits are given identical inputs, we propagate this knowledge through the circuits from the inputs to the outputs. The result is the knowledge of how the outputs of the two circuits correspond, e.g., are the outputs of the two circuits pairwise equivalent? The circuits and the movements of cuts can be described using Boolean formulae.

Symbolic model checking is a technique for verifying temporal specifications of finite state machines. It is well known how finite state machines and the evaluation of the temporal specifications can be expressed using Boolean formulae. We show how to do these manipulations using BEDs. We concentrate on examples which are hard for standard symbolic model checking methods.

Determining whether a formula is satisfiability is a problem which occurs in verification of combinational circuits and in symbolic model checking. Often satisfiability checking is associated with detecting errors. We examine how satisfiability checking can be done using the BED data structure.

Finally, we take a look at how it is possible to extend the BED data structure. Among other operations, we introduce an operator for computing minimal p-cuts in fault trees. A fault tree is a Boolean formula expressing whether a system fails based on the condition (“failure” or “working”) of each of the components. A minimal p-cut is a representation of the most likely reasons for system failure. This method can be used to calculate approximately the probability of system failure given the failure probabilities of each of the components.

As part of this research, we have developed a BED package. The appendix describes the package from a user’s point of view.

Equivalence checking of combinational circuits is a formal verification problem which translates into tautology checking of Boolean formulae. Using BEDs we are able to preserve much of the structure of the circuits within the Boolean formulae. We show how to exploit the structural information in the verification process.

Sometimes combinational circuits are specified in a hierarchical or modular way. We present a method for verifying equivalence between two such circuits. The method builds on cut propagation. Assuming that the two circuits are given identical inputs, we propagate this knowledge through the circuits from the inputs to the outputs. The result is the knowledge of how the outputs of the two circuits correspond, e.g., are the outputs of the two circuits pairwise equivalent? The circuits and the movements of cuts can be described using Boolean formulae.

Symbolic model checking is a technique for verifying temporal specifications of finite state machines. It is well known how finite state machines and the evaluation of the temporal specifications can be expressed using Boolean formulae. We show how to do these manipulations using BEDs. We concentrate on examples which are hard for standard symbolic model checking methods.

Determining whether a formula is satisfiability is a problem which occurs in verification of combinational circuits and in symbolic model checking. Often satisfiability checking is associated with detecting errors. We examine how satisfiability checking can be done using the BED data structure.

Finally, we take a look at how it is possible to extend the BED data structure. Among other operations, we introduce an operator for computing minimal p-cuts in fault trees. A fault tree is a Boolean formula expressing whether a system fails based on the condition (“failure” or “working”) of each of the components. A minimal p-cut is a representation of the most likely reasons for system failure. This method can be used to calculate approximately the probability of system failure given the failure probabilities of each of the components.

As part of this research, we have developed a BED package. The appendix describes the package from a user’s point of view.

##### MSC:

68-02 | Research exposition (monographs, survey articles) pertaining to computer science |

68Q60 | Specification and verification (program logics, model checking, etc.) |

PDF
BibTeX
XML
Cite

\textit{P. F. Williams}, Formal verification based on Boolean expression diagrams. Amsterdam: Elsevier; Lyngby: TU Denmark, Department of Information Technology (Diss. 2000) (2001; Zbl 1266.68004)

Full Text:
DOI

##### References:

[1] | P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT solvers. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2000. 5.1, 5.3.1, 20, 5.6, 5.6 · Zbl 0971.68633 |

[2] | P. Ashar, A. Ghosh, and S. Devadas. Boolean satisfiability and equivalence checking using general binary decision diagrams. In Proc. International Conf. Computer Design (ICCD), pages 259-264. IEEE Computer Society Press, 1991. 7 |

[3] | H. R. Andersen and H. Hulgaard. Boolean expression diagrams. Information and Computation. (To appear). 2, 2.2, 2.3, 2, 7 · Zbl 1096.68053 |

[4] | H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In IEEE Symposium on Logic in Computer Science (LICS), July 1997. 2, 2.2, 2.3, 6, 7 · Zbl 1096.68053 |

[5] | Akers, S.B., Binary decision diagrams, IEEE transactions on computers, 27, 6, 509-516, (June 1978), 2.4 |

[6] | R. E. Bryant, D. L. Beatty, and C.-J. H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 397-402, June 1991. 5.6 |

[7] | R. E. Bryant, and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 535-541, 1995. 2.4, 7, 7, 3.6 |

[8] | A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. ACM/IEEE Design Automation Conference (DAC), 1999. 3.2.3, 5.1, 5.3.2, 5.5, 5.6 |

[9] | A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science. Springer-Verlag, 1999. 3.2.3, 5.1, 5.5, 5.6 |

[10] | Burch, J.R.; Clarke, E.M.; Long, D.E.; MacMillan, K.L.; Dill, D.L., Symbolic model checking for sequential circuit verification, IEEE transactions on computer-aided design of integrated circuits and systems, 13, 4, 401-424, (April 1994), 5.3.1 |

[11] | Burch, J.R.; Clarke, E.M.; McMillan, K.L.; Dill, D.L.; Hwang, L.J., Symbolic model checking: 10^20 states and beyond, Information and computation, 98, 2, 142-170, (June 1992), 5.1, 5.6 |

[12] | A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In Computer Aided Verification (CAV), volume 1633 of Lecture Notes in Computer Science. Springer-Verlag, 1999. 3.2.3, 5.1, 5.5, 5.6 · Zbl 1046.68578 |

[13] | B. Becker and R. Drechsler. Decision diagrams in synthesis — algorithms, applications and extensions. In VLSI Design Conference, pages 46-50, Hyderabad, January 1997. 2.4 |

[14] | F. Brglez and H. Fujiware. A neutral netlist of 10 combinational benchmarks circuits and a target translator in Fortran. In Special Session International Symposium on Circuits and Systems (ISCAS), 1985. 3.2.4, 3.5.1, 22 |

[15] | R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hactel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 188-191, 1993. 7, 3.6 |

[16] | P. Bjesse. Symbolic model checking with sets of states represented as formulas. Technical Report CS-1999-102, Chalmers University of Technology, Sweden, June 1999. 3.2.3 · Zbl 1046.68639 |

[17] | D. Brand. Verification of large synthesized designs. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 534-537, 1993. 10, 3.7, 3.6 |

[18] | K. Brace, R. Rudell, and R. Bryant. Efficient implementation of a BDD package. In Proceedings of the 27th ACM/IEEE Design Automation Conference. IEEE 0738, 1990. 2.1 |

[19] | K. M. Butler, D. E. Ross, R. Kapur, and M. R. Mercer. Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams. In Proc. ACM/IEEE Design Automation Conference (DAC), number 28, pages 417-420, 1991. 3.3 |

[20] | Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE transactions on computers, 35, 8, 677-691, (August 1986), 2, 2.2, 2.2, 2.2, 6, 2.4, 7, 3.5.1, 5.1, 7.4.1 |

[21] | Bryant, R.E., Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM computing surveys, 24, 3, 293-318, (September 1992), 2, 2.2, 2.2, 6, 7 |

[22] | R. E. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 236-243, November 1995. 2.4 |

[23] | O. Coudert, C. Berthet, and J.C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 365-373, Grenoble, France, June 1989. Springer-Verlag. 3.2.3, 5.3.1 |

[24] | A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. N \({\scU}\)SMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 495-499, Trento, Italy, July 1999. Springer-Verlag. 5.4 · Zbl 1046.68587 |

[25] | Clarke, E.M.; Emerson, E.A.; Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM transactions on programming languages and systems, 8, 2, 244-263, (April 1986), 5.2.1, 5.6 |

[26] | E. M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 159-163, Los Alamitos, Ca., USA, November 1995. IEEE Computer Society Press. 7 |

[27] | Clarke, E.M.; Grumberg, O.; Peled, D., Model checking, (1999), The MIT Press Cambridge, MA, 16, 5.6 |

[28] | Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate quantified Boolean formulae. In Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98), pages 262-267, Menlo Park, July 1998. AAAI Press. 5.6 · Zbl 0979.68124 |

[29] | P.-Y. Chung, I. N. Hajj, and J. H. Patel. Efficient variable ordering heuristics for shared ROBDD. In Proc. International Symposium on Circuits and Systems (ISCAS), pages 1690-1693, 1993. 3.3, 3.3.1 |

[30] | Cormen, T.H.; Leiserson, C.E.; Rivest, R.L., Introduction to algorithms, (1990), MIT Press, 2.2, 3.4.1 · Zbl 1158.68538 |

[31] | E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. In Proc. International Conf. Computer-Aided Design (ICCAD), 1990. 3.6, 4.5 |

[32] | E. M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang. Spectral transforms for large boolean functions with application to technology mapping. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 54-60, 1993. 7, 3.6 |

[33] | Clarke, E.M.; Wing, J.M., Formal methods: state of the art and future directions, ACM computing surveys, 28, 4, 626-643, (December 1996), 1.3 |

[34] | R. Drechsler, B. Becker, and S. Ruppertz. K^*BMDs: a new data structure for verification. In IFI WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Frankfurt, Germany, October 1995. 7 |

[35] | Drechsler, R.; Becker, B.; Ruppertz, S., The K^*BMD: A verification data structure, IEEE design and test of computers, 14, 2, 51-59, (1997), 2.4, 7 |

[36] | R. Drechsler, B. Becker, and S. Ruppertz. Manipulation algorithms for K^*BMDs. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1217 of Lecture Notes in Computer Science, pages 4-18. Springer-Verlag, 1997. 7 |

[37] | Davis, M.; Longemann, G.; Loveland, D., A machine program for theorem-proving, Communications of the ACM, 5, 7, 394-397, (July 1962), 5.6, 6.2, 6.5 |

[38] | Davis, M.; Putnam, H., A computing procedure for quantification theory, Journal of the ACM, 7, 201-215, (1960), 5.6, 6.2, 6.5 · Zbl 0212.34203 |

[39] | Dutuit, Y.; Rauzy, A., Exact and truncated computations of prime implicants of coherent and noncoherent fault trees within aralia, Reliability engineering and system safety, 58, 2, 127-144, (1997), 7.3, 28, 7.3.2, 7.3.1, 7.5 |

[40] | Y. Dutuit and A. Rauzy. Polynomial approximations of boolean functions by means of positive binary decision diagrams. In Lydersen, Hansen, and Sandtorv, editors, Proceedings of European Safety and Reliability Association Conference, ESREL’98, pages 1467-1472. Balkerna, Rotterdam, 1998. ISBN 90 54 10 966 1. 7.3, 28, 7.3.1, 7.5 |

[41] | R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski. Efficient representation and manipulation of switching functions based on ordered kronecker functional decision diagrams. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 415-419, 1994. 7, 3.6 |

[42] | M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of boolean comparison method based on binary decision diagrams. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 2-5, November 1988. 3.3, 3.3.1 |

[43] | M. Fujita, Y. Matsunga, and T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level synthesis. In Proc. European Conference on Design Automation (EDAC), pages 50-54, 1991. 5, 7 |

[44] | H. Fujii, G. Ootomo, and C. Hori. Interleaving based variable ordering methods for ordered binary decision diagrams. In Proc. International Conf. Computer-Aided Design (ICCAD), 1993. 3.3 |

[45] | M. Fujita. Verification of arithmetic circuits by comparing two similar circuits. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, pages 159-168. Springer-Verlag, 1996. 1.3, 3.1 |

[46] | M. Ganai and A. Kuehlmann. On-the-fly compression of logical circuits. In Proc. of International Workshop on Logic Synthesis, Dana Point, CA, June 2000. 3.6 |

[47] | E. I. Goldberg, Y. Kukimoto, and R. K. Brayton. Canonical TBDD’s and their application to combinational verification. In Proc. International Workshop on Logic Synthesis, 1997. 3.6 |

[48] | Gergov, J.; Meinel, C., Efficient Boolean manipulation with OBDD’s can be extended to FBDD’s, IEEE transactions on computers, 43, 10, 1197-1209, (October 1994), 7, 3.6 |

[49] | H. Grauslund. Linear decision diagrams. Master’s thesis, Department of Information Technology, Technical University of Denmark, Denmark, May 2000. Reference IT-E 843. 2.4, 7 |

[50] | E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to non-clausal formulas. In Proc. Italian National Conference on Artificial Intelligence, volume 1792 of Lecture Notes in Computer Science, Bologna, Italy, September 1999. Springer-Verlag. 5.6, 6.5, 8.1 · Zbl 0961.03014 |

[51] | Gupta, A., Formal hardware verification methods: A survey, Formal methods in system design, 1, 2/3, 151-238, (October 1992), 1.3 |

[52] | J. Harrison. Staalmarck’s algorithm as a HOL derived rule. Lecture Notes in Computer Science, 1125:221-234, 1996. 3.5.3, 3.13 |

[53] | Hughes, G.E.; Cresswell, M.J., An introduction to modal logic, (1974), Methuen & Co. Ltd London, 16 |

[54] | A. Hett, R. Drechsler, and B. Becker. MORE: Alternative implementation of BDD-pakages by multi-operand synthesis. In European Design Conference, 1996. 7, 7.5 |

[55] | A. Hett, R. Drechsler, and B. Becker. Fast and efficient construction of BDDs by reordering based synthesis. In IEEE European Design & Test Conference, 1997. 7, 7.5 |

[56] | Hoffmann, C.M.; O’Donnell, M.J., Pattern matching in trees, Journal of the ACM, 29, 1, 68-95, (January 1982), 3.2.2 |

[57] | H. Hulgaard, P. F. Williams, and H. R. Andersen. Combinational logic-level verification using boolean expression diagrams. In 3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design, September 1997. 1.5, 3 |

[58] | Hulgaard, H.; Williams, P.F.; Andersen, H.R., Equivalence checking of combinational circuits using Boolean expression diagrams, IEEE transactions on computer aided design, (July 1999), 1.5, 3 |

[59] | Jain, J.; Bitner, J.; Abadir, M.S.; Abraham, J.A.; Fussell, D.S., Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functions, IEEE transactions on computers, 46, 11, 1230-1245, (November 1997), 7, 3.6 |

[60] | J. Jain, R. Mukherjee, and M. Fujita. Advanced verification techniques based on learning. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 629-634, 1995. 3.6 |

[61] | S.-W. Jeong, B. Plessier, G. D. Hactel, and F. Somenzi. Extended BDD’s: Trading off canonicity for structure in verification algorithms. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 464-467, 1991. 7, 7, 3.3, 3.3.1, 7.5 |

[62] | A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In Proc. ACM/IEEE Design Automation Conference (DAC), volume 34, pages 263-268, 1997. 3.6 |

[63] | Kunz, W.; Pradhan, D.K., Recursive learning: A new implication technique for efficient solutions to CAD problems — test, verification, and optimization, IEEE transactions on computer aided design, 13, 9, 1143-1158, (September 1994), 3.5.1, 3.6 |

[64] | Kunz, W.; Pradhan, D.K.; Reddy, S.M., A novel frame-work for logic verification in a synthesis environment, IEEE transactions on computer aided design, 15, 1, 20-32, (January 1996), 10, 3.6 |

[65] | U. Kebschull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In Proc. European Conference on Design Automation (EDAC), pages 43-47, 1992. 7, 3.6 |

[66] | W. Kunz. HANNIBAL: An efficient tool for logic verification based on recursive learning. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 538-543, 1993. 3.6 |

[67] | N. Leveson. Building safety into computer controlled systems. Talk at Carnegie Mellon University, November 1999. For more information, visit Dr. Leveson’s website at http://sunnyday.mit.edu. 1.4 |

[68] | Lai, Y.T.; Pedram, M.; Vrudhula, S.B.K., EVBDD-based algorithms for linear integer programming, spectral transformation and function decomposition, IEEE transactions on computer aided design, 13, 8, 959-975, (August 1994), 7, 7 |

[69] | Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 629-634, 1996. 10, 3.6 |

[70] | McMillan, K.L., Symbolic model checking, (1993), Kluwer Academic Publishers, 5.1, 16, 5.2.2, 5.3 · Zbl 0784.68004 |

[71] | S. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 272-277, 1993. 7, 7.3 |

[72] | Minato, S., Binary decision diagrams and applications for VLSI CAD, (1996), Kluwer Academic Publishers, 7, 3.3, 3.3.2 |

[73] | J. Møller and J. Lichtcnberg. Difference decision diagrams. Master’s thesis, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark, August 1998. 2.4, 7 |

[74] | J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proceedings 13th International Workshop on Computer Science Logic, \bfvolume 1683 of Lecture Notes in Computer Science, pages 111-125, Madrid, Spain, September 1999. 2.4, 7 · Zbl 0944.68040 |

[75] | Marques-Silva, J.P.; Sakallah, K.A., GRASP: A search algorithm for propositional satisfiability, IEEE transactions on computers, 48, (1999), 14, 5.3.2, 23 · Zbl 1392.68388 |

[76] | R. Mukherjee, K. Takayama, J. Jain, M. Fujita, J. A. Abraham, and D. S. Fussell. Flover: Filtering oriented combinational verification approach. In Proc. International Workshop on Logic Synthesis, May 1997. 10 |

[77] | S. Malik, A. R. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 6-9, 1988. 3.3, 3.3.1 |

[78] | H. Ochi, K. Yasuoka, and S. Yajima. Breadth-first manipulation of very large binary-decision diagrams. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 48-55, 1993. 7.4.1 |

[79] | Papadimitriou, C.H., Computational complexity, (1994), Addison-Wesley New York, 28 · Zbl 0833.68049 |

[80] | D. K. Pradhan, D. Paul, and M. Chatterjee. VERILAT: Verification using logic augmentation and transformations. In Proc. International Conf. Computer-Aided Design (ICCAD), November 1996. 10, 3.6 |

[81] | M. Richards. A tautology checker loosely related to Stålmarck’s algorithm. Talk at seminar given at Cambridge, March 1998. 3.6 |

[82] | J. T. Rintanen. Improvements to the evaluation of quantified boolean formulae. In D. Thomas, editor, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99-Vol2), pages 1192-1197. Morgan Kaufmann Publishers, August 1999. 5.6 |

[83] | R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 42-47, 1993. 5 |

[84] | E. Sentovich et al. SIS: A system for sequential circuit synthesis. Technical Report Memorandum No. UCB/ERL M92/41, Electronics Research Laboratory, Dept. of EECS, University of California, Berkeley, 1992. 3.5.2 |

[85] | Shen, A.; Devadas, S.; Ghosh, A., Probabilistic manipulation of Boolean functions using free Boolean diagrams, IEEE transactions on computer aided design, 14, (1995), 7 |

[86] | Sebastiani, R., Applying GSAT to non-clausal formulas, Journal of artificial intelligence research (JAIR), 1, 309-314, (January 1994), 5.6, 6.5, 8.1 |

[87] | O. Shtrichman. Tuning SAT checkers for bounded model checking. In Computer Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 480-494, Chicago, U.S.A., July 2000. Springer-Verlag. 8.1 · Zbl 0974.68565 |

[88] | B. Selman, H. J. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In P. Rosenbloom and P. Szolovits, editors, Proc. Tenth National Conference on Artificial Intelligence, pages 440-446, Menlo Park, California, 1992. American Association for Artificial Intelligence, AAAI Press. 5.6, 6.5 |

[89] | F. Somenzi. CUDD: CU Decision Diagram Package version 2.3.0. University of Colorado at Boulder, September 1998. http://vlsi.colorado.edu/ fabio. 10 |

[90] | M. Sheeran and G. Stålmarck. A tutorial on Stålmarck’s proof procedure for propositional logic. In G. Gopalakrishnan and P. J. Windley, editors, Proc. Formal Methods in Computer-Aided Design, Second International Conference, FMCAD’98, Palo Alto/CA, USA, volume 1522 of Lecture Notes in Computer Science, pages 82-99, November 1998. 3.4, 3.6, 5.6 |

[91] | Sieling, D.; Wegener, I., Graph driven BDDs — a new data structure for Boolean functions, Theoretical computer science, 141, 1-2, 283-310, (1995), 7, 3.6 · Zbl 0873.68036 |

[92] | T. E. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In J.P. Jouannaud, editor, 1st International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, September 1994. 3.6 |

[93] | C.A.J. van Eijk. Formal Methods for the Verification of Digital Circuits. PhD thesis, Technische Universitet Eindhoven, 1997. 10, 3.6 |

[94] | C.A.J. van Eijk. Sequential equivalence checking without state space traversal. In Proc. International Conf. on Design Automation and Test of Electronic-based Systems (DATE), 1998. 1.3, 3.1 |

[95] | C.A.J. van Eijk, and G. L. J. M. Janssen. Exploiting structural similarities in a BDD-based verification method. In Theorem Provers in Circuit Design, \bfvolume 901 of Lecture Notes in Computer Science, pages 110-125. Springer-Verlag, 1994. 3.6 |

[96] | Vrudhula, S.B.K.; Pedram, M.; Lai, Y.T., Edge valued binary decision diagrams, (1996), Kluwer Academic Publishers, 7, 7 |

[97] | P. F. Williams, H. R. Andersen, and H. Hulgaard. Satisfiability checking using boolean expression diagrams. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, 2001. 1.5, 6 · Zbl 0978.68563 |

[98] | P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Computer Aided Verification (CAV), \bfvolume 1855 of Lecture Notes in Computer Science, pages 124-138, Chicago, U.S.A., July 2000. Springer-Verlag. 1.5, 5 · Zbl 0974.68526 |

[99] | P. F. Williams, H. Hulgaard, and H. R. Andersen. Equivalence checking of hierarchical combinational circuits. In IEEE International Conference on Electronics, Circuits and Systems (ICECS), September 1999. 1.5, 4 |

[100] | P. F. Williams. Formal Verification Based on Boolean Expression Diagrams. PhD thesis, Dept. of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000. ISBN 87-89112-59-8. (document) · Zbl 1266.68004 |

[101] | Williams, P.F.; Nikolskaïa, M.; Rauzy, A., Bypassing BDD construction for reliability analysis, Information processing letters, 75, 1-2, 85-89, (July 2000), 1.5, 7.3 |

[102] | B. Yang, Y.-A. Chen, R. E. Bryant, and, D. R. O’Hallaron. Space- and time-efficient BDD construction by working set control. In Asian-Pacific Design Automation Conference (ASPDAC), pages 423-432, February 1998. 3.5.1, 7.4.1 |

[103] | H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, \bfvolume 1249 of Lecture Notes in Artificial Intelligence, pages 272-275, Berlin, July 1997. Springer-Verlag. 15, 5.3.2, 23 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.