Skip to main content
SpringerLink
Log in

Structuring and automating hardware proofs in a higher-order theorem-proving environment

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

In this article we present a structured approach to formal hardware verification by modeling circuits at the register-transfer level using a restricted form of higher-order logic. This restricted form of higher-order logic is sufficient for obtaining succinct descriptions of hierarchically designed register-transfer circuits. By exploiting the structure of the underlying hardware proofs and limiting the form of descriptions used, we have attained nearly complete automation in proving the equivalences of the specifications and implementations. A hardware-specific tool called MEPHISTO converts the original goal into a set of simpler subgoals, which are then automatically solved by a general-purpose, first-order prover called FAUST. Furthermore, the complete verification framework is being integrated within a commercial VLSI CAD framework.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. G. Birtwistle and P.A. Subrahmanyam (eds.).Current Trends in Hardware Verification and Automated Theorem Proving. Springer Verlag, 1988.

  2. P. Camurati and P. Prinetto. Formal verification of hardware correctness: Introduction and survey of current research.IEEE Computer, 8–19 (July 1988).

  3. V. Stavridou, H. Barringer, and D.A. Edwards. Formal specification and verification of hardware: A comparative case study.Proceedings of the 25th Design Automation Conference (DAC 88) pp. 197–204, 1988.

  4. D. Gajski and R. Kuhn. Guest editors' introduction: New VLSI tools.Computer, 16(12):11–14 (December 1983).

    Google Scholar 

  5. R.A. Walker and D.E. Thomas. A model of design representation and synthesis.Proceedings of the 22nd DAC, pp. 453–457, 1985.

  6. A. Cohn. The notion of proof in hardware verification.Journal of Automated Reasoning, 5:127–139 (1989).

    Google Scholar 

  7. O. Coudert, C. Berthet, and J.C. Madre. Verification of synchronous sequential machines based on symbolic execution.Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989.

  8. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond.Proceedings of the 5th Annual Symposium on Logic in Computer Science, 1990.

  9. Th. Kropf and H.-J. Wunderlich. A common approach to test generation and hardware-verification based on temporal logic.Proceedings of the International Test Conference (ITC 91), Nashville, pp. 57–66, October 1991.

  10. J.R. Burch, E.M. Clarke, and D.E. Long. Representing circuits more efficiently in symbolic model checking.Proceedings of the 28th Design Automation Conference (DAC 91), pp. 403–407, 1991.

  11. N.C.E. Srinivas and V.D. Agrawal. Prove: Prolog based verifier.Proceedings of the International Conference on Computer Aided Design, pp. 306–309, 1986.

  12. R.S. Boyer and J.S. Moore:A Computational Logic Handbook. Academic Press, Boston, 1988.

    Google Scholar 

  13. L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated reasoning: Introduction and applications. Prentice-Hall, Englewood Cliffs, NJ, 1984.

    Google Scholar 

  14. C.M. Angelo, D. Verkest, L. Claesen, and H. De Man. Formal hardware verification inHOL and in Boyer-Moore: A comparative analysis.Proceedings of the 1991 International Workshop on the HOLTheorem Proving System and its Applications. IEEE Press, 1991, Davis, CA, pp. 340–347.

    Google Scholar 

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

    Google Scholar 

  16. M.J.C. Gordon. A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam (eds.), VLSI Specification, Verification and Synthesis. Kluwer, Boston, 1988.

    Google Scholar 

  17. M.J.C. Gordon, R. Milner, and C.P. Wadsworth. A mechanized logic of computation.Lecture Notes in Computer Science, 78:(1979).

  18. M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam (eds.),Formal Aspects of VLSI Design. North-Holland, Amsterdam, 1986.

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

  20. Proceedings of the Third HOLUsers Meeting, Aarhus University, October 1990.

  21. Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, University of California, Davis, August 1991. IEEE Press, 1991.

  22. A. Cohn. A proof of correctness of the Viper microprocessor: The first level. In G. Birtwistle and P.A. Subrahmanyam (eds.),VLSI Specification, Verification and Synthesis, Kluwer, 1988.

  23. A. Cohn. Correctness properties of the Viper block Model: The second level.Current Trends in Hardware Verification and Automated Theorem Proving. Springer Verlag, 1988.

  24. W.J. Cullyer. Implementing safety critical systems: The VIPER microprocessor. In G. Birtwistle and P.A. Subrahmanyam (eds.),VLSI Specification, Verification and Synthesis. Kluwer, Boston, 1988.

    Google Scholar 

  25. J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwistle and P.A. Subrahmanyam (eds.),VLSI Specification, Verification and Synthesis. Kluwer, Boston, 1988.

    Google Scholar 

  26. F.K. Hanna, M. Longley, and N. Daeche. Formal synthesis of digital systems. In L.M.J. Claesen (ed.),Applied Formal Methods for Correct VLSI Design. North Holland, Amsterdam, 1989.

  27. M. Aargaard and M. Leeser. A methodology for reusable hardware-proofs.Proceedings of an International Workshop on Higher Order Logic Theorem Proving and its Applications, pp. 127–146, Leuven, Belgium, September 1992.

  28. P. Windley. Microprocessor verification.Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications. IEEE Press, 1991, pp. 32–37.

  29. S. Finn, M. Fourman, M. Francis, and B. Harris. Formal system design — Interactive synthesis based on computer assisted formal reasoning.Proceedings of the International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, November 1989.

  30. E. Mayger and M.P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer (eds.),Proceedings of the International Conference on Very Large Scale Integration. Edinburgh, 1991, pp. 3a.2.1–3a.2.11.

  31. K. Schneider, R. Kumar, and T. Kropf. Structuring hardware proofs: First steps towards automation in a higher-order environment. In A. Halaas and P.B. Denyer (eds.),Proceedings of the International Conference on Very Large Scale Integration, Edinburgh, 1991, pp. 3a.4.1–3a.4.10.

  32. R. Kumar, T. Kropf, and K. Schneider. First steps towards automating hardware proofs in HOL.Proceedings of the 1991 International Workshop on the HOLTheorem Proving System and its Applications. IEEE Press, 1991, pp. 190–193.

  33. K. Schneider, R. Kumar, and T. Kropf. Automating most parts of hardware proofs in HOL. In K.G. Larsen and A. Skou (eds.),In Proceedings of the Workshop on Computer Aided Verification, Aalborg.Lecture Notes in Computer Science, 575:365–375 (1991).

  34. R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment.Proceedings of the 1991 International Workshop on the HOLTheorem Proving System and its Applications. IEEE Press, 1991, pp. 170–176.

  35. K. Schneider, R. Kumar, and T. Kropf. The FAUST-prover.Proceedings of the Conference on Automated Deduction, CADE-11, Albany, NY, 1992.

  36. R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel: The HOL verification of ELLA designs.Proceedings of an International Workshop on Formal Methods in VLSI Design, Miami, January 1991.

  37. S. Kalvala, M. Archer, and K. Levitt. A methodology for integrating hardware design and verification.Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami, January 1991.

  38. M.J.C. Gordon, T. Melham, D. Shepherd, and A. Boulton. The UNWIND library. Manual of the UNWIND library in the HOL system.

  39. M. Fitting.First-Order Logic and Automated Theorem Proving. Springer Verlag, 1990.

  40. K. Schneider, R. Kumar, and T. Kropf. Modelling generic hardware structures by abstract datatypes.Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, pp. 419–429, September 1992.

  41. G. Gentzen. Untersuchungen über das logisches Schließen.Mathematische Zeitschrift, 1:176–210, 1935.

    Google Scholar 

  42. J.H. Gallier.Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Computer Science and Technology Series No. 5, Harper & Row, New York, 1986.

    Google Scholar 

  43. F. Oppacher and E. Suen. HARP: A tableaux-based theorem prover.Journal of Automated Reasoning, 4:69–100 (1988).

    Google Scholar 

  44. S.V. Reeves. Semantic tableau as a framework for automated theorem proving. Department of Computer Science and Statistics, Queen Mary College, University of London, 1987.

  45. A. Church. A note on the Entscheidungsproblem,Journal of Symbolic Logic 1:(1936).

  46. J.A. Robinson. A machine-oriented logic based on the resolution principle.Journal of the ACM, 12:23–41 (1965).

    Google Scholar 

  47. K. Schneider.Ein Sequenzenkalkül für HOL. Diploma thesis, Institute for Computer Design and Fault Tolerance, University of Karlsruhe, 1991.

  48. K. Schneider, R. Kumar, and T. Kropf. Efficient representation and computation of tableau proofs.Proceedings of the Workshop on the HOLTheorem Proving System and its Applications, Leuven, pp. 471–493, September 1992.

  49. R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in PROLOG.Proceedings of 9th Conference on Automated Deduction. Springer Verlag, (1988).

  50. F.J. Pelletier. Seventy-five problems for testing automatic theorem provers.Journal of Automated Reasoning, 2:191–216 (1986).

    Google Scholar 

  51. J. Joyce.Multilevel Verification of Microprocessor-Based Systems. Ph.D. thesis, University of Cambridge, 1989.

  52. H. Vogelsang. Hardware Verification mit Otter. Studienarbeit, Institut für Rechnerentwurf und Fehlertoleranz, Universität Karlsruhe, June, 1991.

  53. P. Camurati, T. Margaria, and P. Prinetto. Resolution-based correctness proofs of synchronous circuits.Proceedings of the European Design Automation Conference (EDAC 91), pp. 11–15, Amsterdam, 1991.

  54. G. Huet. The undecidability of unification in third order logic.Information and Control, 22(3):257–367 (1973).

    Google Scholar 

  55. D. Goldfarb. The undecidability of the second order unification.Journal of Theoretical Computer Science, 13:225–230 (1981).

    Google Scholar 

  56. W. Bibel.Automated Theorem Proving. Vieweg, 1982.

  57. R. Arthan. Private communication, 1991.

Download references

Author information

Authors and Affiliations

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

    Ramayya Kumar, Klaus Schneider & Thomas Kropf

Authors
  1. Ramayya Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Schneider
    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

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kumar, R., Schneider, K. & Kropf, T. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Form Method Syst Des 2, 165–223 (1993). https://doi.org/10.1007/BF01383880

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01383880

Keywords

Search

Navigation