Logo image
Back
A layered real-time specification of a RISC processor
Book chapter   Peer reviewed

A layered real-time specification of a RISC processor

Peter Kearney and Mark Utting
Formal Techniques in Real Time and Fault Tolerant Systems: Third International Symposium Organized Jointly with the Working Group Provably Correct Systems 1994 Proceedings, pp.455-475
International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems Organized Jointly with the Working Group Provably Correct Systems, ProCoS, 3rd (Lubeck, Germany, 19-Sep-1994–23-Sep-1994)
Lecture Notes in Computer Science (LNCS), 939, Springer Berlin Heidelberg
1994
DOI: https://doi.org/10.1007/3-540-58468-4_178
url
https://doi.org/10.1007/3-540-58468-4_178View
Published Version

Abstract

Computer Software Computer Hardware computer science microprogramming memory management
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.

Details

Metrics

741 Record Views
Logo image