Algebraic Models of Correctness for Microprocessors

We present a method of describing microprocessors at different levels of temporal and data abstraction, and consider pipelined and superscalar processors. We model microprocessors using iterated maps, defined by equations which evolve a system from an initial state by the iterative application of a next-state function. Levels of timing abstraction are related by temporal abstraction maps called retimings. We state correctness conditions for microprogrammed, pipelined and superscalar processors. We introduce one-step theorems that permit verification of correctness conditions to be considerably simplified under well-defined conditions. We extend the one-step theorems to superscalar microprocessors.