Models of Superscalar Microprocessors

Neal Harman

(University of Wales Swansea)

Superscalar microprocessors - which include all current PowerPCs, Alphas, Intel processors, and SPARCs - attempt to issue multiple instructions within a single clock cycle, and may internally reorder instruction execution. The talk will consider how we can model the behaviour of superscalar microprocessors, and formalise and prove their correctness with respect to an architectural description. Superscalar processors are more complex to model than non-superscalar examples, and require a different correctness model because the temporal ordering of events can change between levels of abstraction. The talk will introduce techniques for algebraically modelling microprocessors; discuss informally the operation of pipelined and superscalar; show how our models must be changed to accomodate superscalar processors; and consider the problems still to be solved.
Friday 26th February 1999, 15:00
Seminar Room 322
Department of Computer Science