Algebraic Models of Simultaneous Multithreaded and Multi-core Processors

Much current work on modelling and verifying microprocessors can accommodate pipelined and superscalar processors. However, superscalar and pipelined processors are no longer state-of-the-art: Simultaneous Multithreaded (SMT) and Multi-core, or Chip-Level Multithreaded (CMT) microprocessors enable a single microprocessor implementation to present itself to the programmer as multiple (virtual in the case of SMT) processors with shared state. This paper builds on a series which has developed a hierarchy of many-sorted algebraic models, able to model a variety of processor types, at nt levels of temporal and data abstraction. These models address both the behavioural definition of microprocessors, and also the question: what does it mean for a microprocessor implemenation to be correct? They also consider how the process of formal verification can be simplified by indentifying some easily-checked preconditions (the one-step theorems). We extend the existing algebraic tools for modeling...

• Type: Conference
• Year: 2007
• Where: CALCO
• Authors: Neal A. Harman
• Keywords: CALCO 2007, Microprocessors, One-step Theorems, Single Microprocessor Implementation