Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
STACS 96 (STACS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1046))

Included in the following conference series:

Abstract

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.

Supported by DFG grants WE 1066/7-2 and 7-3.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. B. Becker, R. Drechsler and R. Werchner: On the relation between BDDs and FDDs. LATIN '95, LNCS 911, 71–83 (1995).

    Google Scholar 

  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. 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. R. E. Bryant: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers 35, 677–691 (1986).

    Google Scholar 

  6. R. E. Bryant: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24, 293–318 (1992).

    Article  Google Scholar 

  7. A. Chandra, L. Stockmeyer and U. Vishkin: Constant depth reducibility. SIAM J. on Computing 13, 423–439 (1984).

    Article  Google Scholar 

  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. J. Gergov and C. Meinel: Efficient Boolean manipulation with OBDDs can be extended to FBDDs. IEEE Trans. on Computers 43, 1197–1209 (1994).

    Article  Google Scholar 

  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. 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. 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. M. Krause: Lower bounds for depth-restricted branching programs. Information and Computation 91, 1–14 (1991).

    Article  Google Scholar 

  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. N. Nisan and A. Wigderson: Rounds in communication complexity revisited. SIAM J. on Computing 22, 211–219 (1993).

    Article  Google Scholar 

  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. D. Sieling and I. Wegener: Graph driven BDDs — a new data structure for Boolean functions. Theoretical Computer Science 141, 283–310 (1995).

    Article  Google Scholar 

  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).

    Article  Google Scholar 

  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. 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. I. Wegener: Efficient data structures for Boolean functions. Discrete Mathematics 136, 347–372 (1994).

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB Informatik, LS II, Univ. Dortmund, 44221, Dortmund, Germany

    Beate Bollig & Ingo Wegener

Authors
  1. Beate Bollig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ingo Wegener
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Puech Rüdiger Reischuk

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bollig, B., Wegener, I. (1996). Read-once projections and formal circuit verification with binary decision diagrams. In: Puech, C., Reischuk, R. (eds) STACS 96. STACS 1996. Lecture Notes in Computer Science, vol 1046. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60922-9_40

Download citation

  • DOI: https://doi.org/10.1007/3-540-60922-9_40

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60922-3

  • Online ISBN: 978-3-540-49723-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation