Algebraic Models of Correctness for Microprocessors

In this paper we present a method of describing microprocessors at different levels of temporal and data abstraction. We consider microprogrammed, pipelined and superscalar processors, in which instructions may complete simultaneously, or out of program order. We model microprocessors by means of iterated maps. These maps are defined by equations which evolve a system from an initial state by the iterative application of a next-state function. A formal model of time is used in the form of a clock algebra. Time is related by temporal abstraction maps called retimings. We state correctness conditions for microprogrammed, pipelined and superscalar microprocessors. We introduce and prove the one step theorem that permits verification of correctness conditions to be considerably simplified under well-defined conditions.

• Type: Journal
• Year: 2000
• Where: FAC
• Authors: Anthony C. J. Fox, Neal A. Harman
• Keywords: Correctness Conditions, FAC 2000, Microprocessors, Superscalar Processors