Skip to main content
SpringerLink
Log in

Abstraction of hardware construction

  • Conference paper
  • First Online:
Higher-Order Algebra, Logic, and Term Rewriting (HOA 1995)

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

Abstract

We concentrate on the foundation of formal hardware construction and present a new hardware-centered concept and methodology. It is a development from, and also contrast to, the traditional logic-centered approach. It introduces a higher-order variable construction model of hardware and the notion of generic construction schemes. We demonstrate how the model and the schemes formalize the construction (and verification as well) for a class of computers, as an example to illustrate our concepts and method.

Li-Guo Wang was supported by a scholarship from Siemens AG Munich and under SERC GR/F 35890.

Michael Mendler was supported by a Human Capital and Mobility fellowship in the EuroForm network

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. D. A. Basin, G. M. Brown, and M. E. Leeser, Formally verified synthesis of combinational CMOS circuits. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, pages 197–206, North-Holland, 1990.

    Google Scholar 

  2. D. A. Basin, Extracting Circuits from Constructive Proofs. In 1991 International Workshop on Formal Verification in VLSI Design. ACM IFIP WG 10.2, Jan. 1991.

    Google Scholar 

  3. G. Birtwistle and B. Graham, Verifying the SECD in HOL. In [32].

    Google Scholar 

  4. G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988.

    Google Scholar 

  5. B. Bose and S. D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor. In [29].

    Google Scholar 

  6. H. Busch, Proof-based transformation of formal hardware models. In [22], pp. 271–296.

    Google Scholar 

  7. K. M. Chandy and J. Mishra, Parallel Program Design. A Foundation. Addison Wesley, 1988.

    Google Scholar 

  8. L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier /North-Holland, 1989.

    Google Scholar 

  9. A. Cohn, A Proof of Correctness of the Viper Microprocessor: First Level. In [4], pp. 27–71.

    Google Scholar 

  10. A. Cohn, Correctness Properties of the Viper Block Model: The Second Level. In G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp.1–91.

    Google Scholar 

  11. M. P. Fourman, R. L. Harris, Lambda-Logic and Mathematics Behind Design Automation, 26th ACM/IEEE Design Automation Conference, 1988.

    Google Scholar 

  12. M. P. Fourman, Formal System Design. In [32], pp 191–236.

    Google Scholar 

  13. M. J. C. Gordon, Proving a Computer Correct with the LCF_LSM Hardware Verification System. Technical Report No. 42, Computer Laboratory, University of Cambridge, 1983.

    Google Scholar 

  14. M. J. C. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware. in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, North-Holland, 1986, pp. 153–177.

    Google Scholar 

  15. M. J. C. Gordon and T. F. Melham, Introduction to HOL. Cambridge University Press, 1993.

    Google Scholar 

  16. F. K. Hanna and N. Daeche, Specification and Verification of Digital Systems using Higher-Order Predicate Logic. IEE Proceedings, Vol. 133, Part E, No. 5, September 1986, pp. 242–254.

    Google Scholar 

  17. F. K. Hanna, M. Longley, and N. Daeche, Formal synthesis of digital systems. In [8], pages 532–548.

    Google Scholar 

  18. F. K. Hanna and N. Daeche, Strongly-Typed Theory of Structure and Behaviors. In [29], pp. 39–54.

    Google Scholar 

  19. N. A. Harman and J. V. Tucker, Algebraic Models and the Correctness of Microprocessors. In [29], pp. 92–108.

    Google Scholar 

  20. J. M. J. Herbert, Incremental Design and Formal Verification of Microcoded Microprocessors. In [34], pp. 157–174.

    Google Scholar 

  21. W. A. Hunt, FM8501, A Verified Microprocessor. Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985.

    Google Scholar 

  22. G. Jones and M. Sheeran, Designing Correct Circuits Springer, 1991.

    Google Scholar 

  23. G. Jones and M. Sheeran, Circuit Design in Ruby. In [32].

    Google Scholar 

  24. J. J. Joyce, Multi-Level Verification of Microprocessor-Based Systems, Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989 (Technical Report No. 195, May 1990).

    Google Scholar 

  25. J. J. Joyce, Generic Specification of Digital Hardware. In [22], pp. 68–91.

    Google Scholar 

  26. J. J. Joyce, G. Birtwistle and M. Gordon, Proving a Computer Correct in Higher Order Logic. Report No. 100, Computer Laboratory, Cambridge University, 1986.

    Google Scholar 

  27. M. Langevin and E. Cerny, Verification of Processor-like Circuits. In Advanced Work on Correct Hardware Design Methodology, Turin, 12–14 June 1991.

    Google Scholar 

  28. T. F. Melham, Abstraction mechanism for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, eds., VLSI Specification, Verification, and Synthesis, pages 267–291. Kluwer Academic Publishers, 1988.

    Google Scholar 

  29. G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, LNCS 683, Springer-Verlag, May 1993.

    Google Scholar 

  30. L. C. Paulson. Isabelle Tutorial and User's Manual, 1990.

    Google Scholar 

  31. M. Srivas and M. Bickford, Formal Verification of a Pipelined Microprocessor, In IEEE Software, September 1990, pp. 52–64.

    Google Scholar 

  32. J. Staunstrup, editor, IFIP WG 10.5 Formal Methods for VLSI Design, North-Holland, 1990.

    Google Scholar 

  33. J. Staunstrup, A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.

    Google Scholar 

  34. V. Stavridou, T. F. Melham, and R. T. Boute, eds., Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP TC10/WG 10.2, North Holland, June 1992.

    Google Scholar 

  35. Dany Suk, Hardware Synthesis in Constructive Type Theory. In G. Jones and M. Sheeran, eds., Designing Correct Circuits, pp 29–49, Oxford, Springer-Verlag, 1990.

    Google Scholar 

  36. S. Tahar and R. Kumar, Towards a Methodology for the Formal Verification of RISC Processors. In Proceedings IEEE International Conference on Computer Design (ICCD'93), 1993, pp. 58–62.

    Google Scholar 

  37. D. Verkest and L. Claesen and H. De Man, On the use of the Boyer-Moore theorem prover for correctness proofs of parametrized hardware modules. In [8], pp. 405–422.

    Google Scholar 

  38. Li-Guo Wang, Synthesis of Nondeterministic Logic Programs, Chinese Journal of Software, Vo. 1, No. 1, ISSN 1000-9825, CN 11-2560, January 1990.

    Google Scholar 

  39. Li-Guo Wang, Formal Derivation of A Class of Computers. PhD Thesis, LFCS, Department of Computer Science, University of Edinburgh, ECS-CST-119-95, September 1995.

    Google Scholar 

  40. Li-Guo Wang and M. Mendler, Formal Derivation of A Class of Computers: Its high stage — abstract microprogramming. In H. Eveking and P. Camurati, eds., Correct Hardware Design and Verification Methods (CHARME'95), Springer LNCS 987, 1995, pp. 84–102.

    Google Scholar 

  41. P. J. Windley, A Hierarchical Methodology for the Verification of Microprogrammed Microprocessors. In IEEE Symposium on Security and Privacy, May 1990.

    Google Scholar 

  42. P. J. Windley, A Theory of Generic Interpreters. In [29], pp. 122–134.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, Scotland, UK

    Li-Guo Wang

  2. Fakultät für Mathematik und Informatik, Universität Passau, Innstraße 33, D-94032, Passau, Deutschland

    Michael Mendler

Authors
  1. Li-Guo Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gilles Dowek Jan Heering Karl Meinke Bernhard Möller

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wang, LG., Mendler, M. (1996). Abstraction of hardware construction. In: Dowek, G., Heering, J., Meinke, K., Möller, B. (eds) Higher-Order Algebra, Logic, and Term Rewriting. HOA 1995. Lecture Notes in Computer Science, vol 1074. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61254-8_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-61254-8_30

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61254-4

  • Online ISBN: 978-3-540-68389-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation