Sciweavers

Share
FAC
2000

Algebraic Models of Correctness for Microprocessors

12 years 1 months ago
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.
Anthony C. J. Fox, Neal A. Harman
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Where FAC
Authors Anthony C. J. Fox, Neal A. Harman
Comments (0)
books