Advertisement

Abstract

This paper gives an overview of the real-time specification of a commercial RISC processor. The specification is at two related levels, with an abstraction relation defined between them. The lower level specification models separate stages of execution of up to five overlapped instructions. The higher level specification abstracts from the lower level to recapture an atomic, instruction level view of code execution. The load word instruction is used as an example to illustrate the specification at both levels.

Keywords

Data Cache Pipeline Stage Program Counter Current Instruction Instruction Cache 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Henman, P. and Staples, J., ‘Introduction to Functional Set Theory', Technical Report 144, Key Centre for Software Technology, Department of Computer Science, University of Queensland, 1990, revised September 1991.Google Scholar
  2. 2.
    Fidge, C., Kearney, P., Utting, M., ‘Formal Specification and Interactive Proof of a Simple Real-time Scheduler', Software Verification Research Centre Technical Report 94-11, April 1994, 49 pages.Google Scholar
  3. 3.
    Gerry Kane and Joe Heinrich, MIPS RISC Architecture, Prentice Hall 1992.Google Scholar
  4. 4.
    Kearney, P., Staples, J., Abbas, A., ‘Functional Verification of Hard Real-Time Programs', in Algorithms, Software, Architecture, ed. L. van Lueewen, Information Processing 92, Volume I, North-Holland 1992, 113–119.Google Scholar
  5. 5.
    Staples, J., Robinson, P., Hazel, D., ‘A functional logic for higher level reasoning about computation', to appear in Formal Aspects of Computing, 6, pages 1–38, 1994.Google Scholar
  6. 6.
    Utting, M., Kearney, P., ‘Pipeline Specification of a MIPS R3000 CPU', Software Verification Research Centre Technical Report 92-6, October 1992, revised February 1994, 57 pages.Google Scholar
  7. 7.
    Utting, M., ‘Instruction-level Specification of a MIPS R3000 CPU', Software Verification Research Centre Technical Report 93-26, February 1994, 27 pages.Google Scholar
  8. 8.
    Utting, M., Kearney., P., Specification Issues for Real-Time Behaviour of RISC Processors. To appear at the Australasian Workshop on Parallel and Real-Time Systems, Melbourne, July 1994.Google Scholar
  9. 9.
    Utting, M., Whitwell, K., ‘Ergo 4.0 Users Manual', Software Verification Research Centre Technical Report 93-19, December 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Peter Kearney
    • 1
  • Mark Utting
    • 1
  1. 1.Software Verification Research CentreUniversity of QueenslandSt. LuciaAustralia

Personalised recommendations