ALGEBRAIC MODELS OF MICROPROCESSORS - ARCHITECTURE AND ORGANIZATION

We present an algebraic method for modeling microprocessors at differe nt levels of abstraction, and for expressing the relationships between each level. We consider microprocessors at levels of abstraction dete rmined by time and details of construction. The algebraic models isola te features of the scientific structure of microprocessor computation. providing: (i) a basis for modular decomposition of the description o f microprocessors, including correctness criteria; and (ii) equational specification and verification techniques for the design of microproc essors relevant to a range of specification languages and theorem prov ers. Our specifications are iterated maps that decompose the modeling of the computer into easily understood, equationally specified stages, represented by algebras. We illustrate our algebraic tools with an ex ample of a simple computer.