Algebraic Models of Correctness for Microprocessors
Anthony C. J. Fox, N. A. Harman · Formal Aspects of Computing · 2000
Abstract. 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.