Read-once projections and formal circuit verification with binary decision diagrams

  • Beate Bollig
  • Ingo Wegener
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1046)


Computational complexity is concerned with the complexity of solving problems and computing functions and not with the complexity of verifying circuit designs. The importance of formal verification is evident. Therefore, the framework of a complexity theory for formal verification with binary decision diagrams is developed. This theory is based on read-once projections. For many problems it is determined whether and how they are related with respect to read-once projections. The result that circuits for squaring may be harder to verify than circuits for multiplication is derived and discussed. It is shown that the class of functions with polynomial-size free binary decision diagrams has no complete problem while for the corresponding classes for the other considered types of binary decision diagrams complete problems are presented.


Boolean Function True Variable Formal Verification Binary Decision Diagram Complete Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Ajtai, L. Babai, A. Hajnal, J. Komlós, P. Pudlák, V. Rödl, E. Szemerédi and G. Turán: Two lower bounds for branching programs. 18. STOC, 30–38 (1986).Google Scholar
  2. 2.
    B. Becker, R. Drechsler and R. Werchner: On the relation between BDDs and FDDs. LATIN '95, LNCS 911, 71–83 (1995).Google Scholar
  3. 3.
    B. Bollig, M. Sauerhoff, D. Sieling and I. Wegener: On the power of different types of restricted branching programs. Submitted to Theoretical Computer Science. Electronic Colloquium in Computational Complexity, TR 94-026 (1994).Google Scholar
  4. 4.
    B. Bollig and I. Wegener: Read-once projections and formal circuit verification with binary decision diagrams. Electronic Colloquium in Computational Complexity, TR 95-045 (1995).Google Scholar
  5. 5.
    R. E. Bryant: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers 35, 677–691 (1986).Google Scholar
  6. 6.
    R. E. Bryant: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24, 293–318 (1992).CrossRefGoogle Scholar
  7. 7.
    A. Chandra, L. Stockmeyer and U. Vishkin: Constant depth reducibility. SIAM J. on Computing 13, 423–439 (1984).CrossRefGoogle Scholar
  8. 8.
    M. R. Garey and D. B. Johnson: Computers and intractability — a guide to the theory of NP-completeness. Freeman, New York 1979.Google Scholar
  9. 9.
    J. Gergov and C. Meinel: Efficient Boolean manipulation with OBDDs can be extended to FBDDs. IEEE Trans. on Computers 43, 1197–1209 (1994).CrossRefGoogle Scholar
  10. 10.
    A. Hajnal, W. Maass, P. Pudlák, M. Szegedy and G. Turán: Threshold circuits of bounded depth. 28. FOCS, 99–110 (1987).Google Scholar
  11. 11.
    J. Jain, M. Abadir, J. Bitner, D. S. Fussell and J. A. Abraham: IBDDs: an efficient functional representation for digital circuits. Proc. European Design Automation Conf., 440–446 (1992).Google Scholar
  12. 12.
    U. Kebschull, E. Schubert and W. Rosenstiel: Multilevel logic synthesis based on functional decision diagrams. Proc. European Design Automation Conf., 43–47 (1992).Google Scholar
  13. 13.
    M. Krause: Lower bounds for depth-restricted branching programs. Information and Computation 91, 1–14 (1991).CrossRefGoogle Scholar
  14. 14.
    M. Krause, C. Meinel and S. Waack: Separating the eraser Turing machine classes L e, NL e, coNL e and P e. MFCS, LNCS 324, 405–413 (1988).Google Scholar
  15. 15.
    N. Nisan and A. Wigderson: Rounds in communication complexity revisited. SIAM J. on Computing 22, 211–219 (1993).CrossRefGoogle Scholar
  16. 16.
    S. Ponzio: A lower bound for integer multiplication with read-once branching programs. 27. STOC, 130–139 (1995) (see also Ph. D. Thesis, MIT/LCS-TR-633. Sept. 1995).Google Scholar
  17. 17.
    D. Sieling and I. Wegener: Graph driven BDDs — a new data structure for Boolean functions. Theoretical Computer Science 141, 283–310 (1995).CrossRefGoogle Scholar
  18. 18.
    K. S. Siu, J. Bruck, T. Kailath and T. Hofmeister: Depth-efficient neural networks for division and related problems. IEEE Trans. on Information Theory 39, 946–956 (1993).CrossRefGoogle Scholar
  19. 19.
    S. Skyum and L. G. Valiant: A complexity theory based on Boolean algebra. Journal of the ACM 32, 484–502 (1985).Google Scholar
  20. 20.
    I. Wegener: Optimal lower bounds on the depth of polynomial-size threshold circuits for some arithmetic functions. Information Processing Letters 46, 85–87 (1993).Google Scholar
  21. 21.
    I. Wegener: Efficient data structures for Boolean functions. Discrete Mathematics 136, 347–372 (1994).CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Beate Bollig
    • 1
  • Ingo Wegener
    • 1
  1. 1.FB Informatik, LS IIUniv. DortmundDortmundGermany

Personalised recommendations