Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Eliminating higher-order quantifiers to obtain decision procedures for hardware verification

  • Conference paper
  • First Online:
Higher Order Logic Theorem Proving and Its Applications (HUG 1993)

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

Included in the following conference series:

Abstract

In this paper, we present methods for eliminating higher-order quantifiers in proof goals arising in the verification of digital circuits. For the description of the circuits, a subset of higher-order logic called hardware formulae is used which is sufficient for describing hardware specifications and implementations at register transfer level. Real circuits can be dealt with as well as abstract (generic) circuits. In case of real circuits, it is formally proved, that the presented transformations result in decidable formulae, such that full automation is achieved for them. Verification goals of abstract circuits can be transformed by the presented methods into goals of logics weaker than higher-order logic, e.g. (temporal) propositional logic. The presented transformations are also capable of dealing with hierarchy and have been implemented in HOL90.

This work has been partly financed by a german national grant, project Automated System Design, SFB No.358.

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.

Similar content being viewed by others

References

  1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390–413, 1935.

    Article  Google Scholar 

  2. P.B. Andrews. A Transfinite Type Theory with Type Variables. North-Holland Publishing Company, 1965.

    Google Scholar 

  3. D. Gabbay and H. J. Ohlbach. Quantifier elimination in second-order predicate logic. Technical Report MPI-I-92-231, Max-Planck-Institut für Informatik, Saarbrücken, July 1992.

    Google Scholar 

  4. M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam, editors, Formal aspects of VLSI Design. North-Holland, 1986.

    Google Scholar 

  5. M.J.C. Gordon. Programming Language Theory and its Implementation. International Series in Computer Science. Prentice Hall, 1988.

    Google Scholar 

  6. A. Gupta. Formal hardware verification methods: A survey. Journal of Formal Methods in System Design, 1:151–238, 1992.

    Google Scholar 

  7. F.K. Hanna and N. Daeche. Specification and verification of digital systems using higher-order predicate logic. IEE Proc. Pt. E, 133(3):242–254, 1986.

    Google Scholar 

  8. S.L.P. Jones. The Implementation of Functional Programming Languages. Prentice Hall, 1987.

    Google Scholar 

  9. J. Joyce. More reasons why higher-order logic is a good formalism for specifying and verifying hardware. In International Workshop on Formal Methods in VLSI Design, Miami, 1991.

    Google Scholar 

  10. R. Kumar, K. Schneider, and Th. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal Methods in System Design, 2(2):165–223, 1993.

    Google Scholar 

  11. K. Schneider, R. Kumar, and Th. Kropf. Structuring hardware proofs: First steps towards automation in a higher-order environment. In P.B. Denyer A. Halaas, editor, International Conference on Very Large Scale Integration, pages 81–90, Edinburg, Edingburgh, 1991. North Holland.

    Google Scholar 

  12. K. Schneider, R. Kumar, and Th. Kropf. Modelling generic hardware structures by abstract datatypes. In L.J.M. Claesen and M.J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions, pages 165–176, Leuven, Belgium, 1992. North-Holland.

    Google Scholar 

  13. K. Schneider, R. Kumar, and Th. Kropf. Alternative proof procedures for finite-state machines in a higher-order environment. In International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Rechnerentwurf und Fehlertoleranz, Universität Karlsruhe, P.O. Box 6980, 76128, Karlsruhe, Germany

    Klaus Schneider & Thomas Kropf

  2. Forschungszentrum Informatik, Haid-und-Neustraße 10-14, 76131, Karlsruhe, Germany

    Ramayya Kumar

Authors
  1. Klaus Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ramayya Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thomas Kropf
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schneider, K., Kumar, R., Kropf, T. (1994). Eliminating higher-order quantifiers to obtain decision procedures for hardware verification. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_150

Download citation

  • DOI: https://doi.org/10.1007/3-540-57826-9_150

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57826-0

  • Online ISBN: 978-3-540-48346-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation