Advertisement

Algebraic models and the correctness of microprocessors

  • N. A. Harman
  • J. V. Tucker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

A general algebraic method for modelling microprocessors at different levels of abstraction by means of iterated maps is introduced, supporting equational specification and design. We apply this iterated map method to the top level Programmer's Model specification, and to an abstract implementation, the Abstract Circuit Design. We formalise what it means for the implementation to correctly implement the specification. We illustrate the iterated map method with a case study.

Keywords

Clock Cycle VLSI Design Memory Word Abstract Data Type Algebraic Specification 
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.

References

  1. G Birtwistle and B Graham, “Verifying SECD in HOL”, pp.129–177 in Formal Methods for VLSI Design, ed. J Staunstrup, North-Holland, (1990).Google Scholar
  2. A Cohn and M Gordon, “A Mechanised Proof of Correctness of a Simple Counter”, pp.65–96 in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990).Google Scholar
  3. A Cohn, “A Proof of Correctness of the VIPER Microprocessor: the First Levels”, pp.27–72 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987).Google Scholar
  4. W J Cullyer, “Implementing Safety Critical Systems: the Viper Microprocessor”, pp.1–26 in VLSI Specification, Verification, and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987).Google Scholar
  5. W J Cullyer, “Application of Formal Methods to the VIPER Microprocessor”, IEE Proceedings, 134 E, 3, pp.133–141 (May 1987).Google Scholar
  6. J S Florentin, Microprogrammed Systems Design, Macmillan, (1991).Google Scholar
  7. A Geser, “A Specification of the Intel 8085 Microprocessor: A Case Study.”, pp.347–402 in Algebraic Methods: Theory, Tools and Applications, ed. M Wirsing and J A Bergstra, Lecture Notes in Computer Science 394, Springer-Verlag, (1989).Google Scholar
  8. M Gordon, “Proving a Computer Correct with the LCF-LSM Hardware Verification System”, Technical Report No. 42, Computer Laboratory, University of Cambridge, (1983).Google Scholar
  9. M Gordon, “HOL: A Proof Generating System for Higher-Order Logic”, pp.73–128 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987).Google Scholar
  10. B Graham and G Birtwistle, “Formalising the Design of an SECD Chip”, pp.40–66 in Hardware Specification, Verification and Synthesis: Mathematical Aspects, ed. M Leeser and G Brown, Lecture Notes in Computer Science 408, Springer Verlag, (1990).Google Scholar
  11. B Graham, The SECD Microprocessor: a Verification Case Study, Kluwer, (1992).Google Scholar
  12. N A Harman and J V Tucker, “Clocks, Retimings, and the Formal Specification of a UART”, pp.375–396 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988).Google Scholar
  13. N A Harman and J V Tucker, “Formal Specification and the Design of Verifiable Computers”, pp.500–503 in Proceedings of the 1988 UK IT Conference, University College Swansea, IEE, (1988).Google Scholar
  14. N A Harman and J V Tucker, “The Formal Specification of a Digital Correlator I: Abstract User Specification”, pp.161–262 in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990).Google Scholar
  15. N A Harman and J V Tucker, “Consistent Refinements of Specifications for Digital Systems”, pp.273–295 in Correct Hardware Design Methodologies, ed. P Prinetto and P Camurati, North-Holland, (1992).Google Scholar
  16. N A Harman, “Formal Specifications for Digital Systems”, Ph.D. Thesis, School of Computer Studies, University of Leeds, (1989).Google Scholar
  17. W A Hunt, “FM8501: A Verified Microprocessor”, The University of Texas at Austin Institute for Computing Science technical report 47, (1986).Google Scholar
  18. S D Johnson and Z Zhu, “An Algebraic Approach to Hardware Specification and Derivation”, in Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, ed. L Claesen, Elsevier, (1991).Google Scholar
  19. J Joyce, “Formal Verification and Implementation of a Microprocessor”, pp.129–159 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987).Google Scholar
  20. P Landin, “On the Mechanical Evaluation of Expressions”, Computer Journal, (1963).Google Scholar
  21. K Meinke and J V Tucker, “Universal Algebra”, pp.189–411 in Handbook of Logic in Computer Science, ed. S Abramsky, D Gabbay, T S E Maibaum, Oxford University Press, (1992).Google Scholar
  22. T Melham, “Using Recursive Types to Reason about Hardware in Higher Order Logic”, pp.27–50 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988).Google Scholar
  23. G J Milne, “Timing Constraints: Formalising their Description and Verification”, in Proceedings of Computer Hardware Description Languages and their Applications, North-Holland, (1989).Google Scholar
  24. G J Milne, “The Formal Description and Verification of Hardware Timing”, University of Strathclyde Computer Science Report HDV-8-90, (1990).Google Scholar
  25. W Stallings, Computer Organisation and Architecture: Principles of Function and Structure, Macmillan, (1987).Google Scholar
  26. V Stavridou, Formal Specification of Digital Systems, Cambridge Tracts in Theoretical Computer Science, CUP (in press), (1993).Google Scholar
  27. P A Subrahmanyam, “Contextual Constraints, Temporal Abstraction and Observational Equivalence in VLSI Design”, pp.159–184 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988).Google Scholar
  28. B C Thompson and J V Tucker, “Equational Specification of Synchronous Concurrent Algebras and Architectures”, Department of Computer Science CSR 9.91, University College Swansea, (1991).Google Scholar
  29. J V Tucker and J I Zucker, Program Correctness over Abstract Data Types with Error State Semantics, North-Holland, (1988).Google Scholar
  30. J V Tucker and J I Zucker, “Generalised Computability and Algebraic Specifications for Abstract Data Types”, In preparation, (1993).Google Scholar
  31. J V Tucker, “Theory of Computation and Specification over Abstract Data Types and its Applications”, in Logic, Algebra and Computation, ed. F L Bauer, Springer, (1991).Google Scholar
  32. W Wechler, “Universal Algebra for Computer Scientists”, EATCS Monograph, Springer-Verlag, Berlin, (1991).Google Scholar
  33. W P Weijland, “Verification of a Systolic Algorithm in Process Algebra”, in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990).Google Scholar
  34. M Wirsing, “Algebraic Specification”, pp.675–788 in Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, ed. J van Leeuwen, Elsevier, (1990).Google Scholar
  35. Z Zhu and S D Johnson, “An Example of Interactive Hardware Transformation”, Indiana University, Computer Science Department (draft), (1991).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • N. A. Harman
    • 1
  • J. V. Tucker
    • 1
  1. 1.Department of Computer ScienceUniversity College of SwanseaSwanseaUK

Personalised recommendations