Algebraic models for advanced microprocessors

• Main Author: Fox, A. C. J.
• Published: Swansea University 1999
• Subjects: 004.01
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.637000

In this thesis, algebraic methods are used to model advanced microprocessor organisations. Correctness is defined by modelling computer systems at two levels of abstraction: the abstract circuit level, and the programmer's model level. The abstract circuit corresponds with a microprocessor organisation, or micro-architecture; and the programmer's model corresponds with a computer architecture. Computer architectures provide stability at the interface between software and hardware; this is achieved by establishing a (relatively) constant target for program compilation, and for future processor development. For commercial viability most new processors must correctly implement an established architecture; in this way the processor guarantees the seamless support of an existing software base. This thesis formally defines the correctness of processors, including those of superscalar design. With the ever increasing need for computing power, superscalar designs are used in many personal computers, and even in embedded applications. Super-scalar designs use long instruction pipelines and multiple functional units to achieve high degrees of instruction-level parallelism; they can execute instructions simultaneously, or in some cases out-of-order. This thesis explores the nature of temporal abstraction for pipelined and super-scalar computer organisations. A superscalar case study is presented; this design provides for out-of-order instruction issue, and uses Thornton's algorithm. This thesis also provides a structured framework for processor verification. With the suitable use of initialisation functions, and temporal abstractions, it is shown that correctness can be verified without the explicit use of temporal induction. In addition to studying the control (temporal) aspects of processors, this thesis also addresses data issues and presents an (abbreviated) algebraic specification of the IEEE-754 floating-point standard.