A Mathematical Model of CPU

Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

A Mathematical Model of CPU

Yatsuka Nakamura: Shinshu University, Nagano
Andrzej Trybulec: Warsaw University, Bialystok
The work has been done while the second author was visiting Nagano in autumn 1992.

Summary.

This paper is based on a previous work of the first author [13] in which a mathematical model of the computer has been presented. The model deals with random access memory, such as RASP of C. C. Elgot and A. Robinson [12], however, it allows for a more realistic modeling of real computers. This new model of computers has been named by the author (Y. Nakamura, [13]) Architecture Model for Instructions (AMI). It is more developed than previous models, both in the description of hardware (e.g., the concept of the program counter, the structure of memory) as well as in the description of instructions (instruction codes, addresses). The structure of AMI over an arbitrary collection of mathematical domains N consists of: \begin{description} \item{ - }a non-empty set of objects, \item{ - }the instruction counter, \item{ - }a non-empty set of objects called instruction locations, \item{ - }a non-empty set of instruction codes, \item{ - }an instruction code for halting, \item{ - }a set of instructions that are ordered pairs with the first element being an instruction code and the second a finite sequence in which members are either objects of the AMI or elements of one of the domains included in N, \item{ - }a function that assigns to every object of AMI its kind that is either {\em an instruction} or {\em an instruction location} or an element of N, \item{ - }a function that assigns to every instruction its execution that is again a function mapping states of AMI into the set of states. \end{description} By a state of AMI we mean a function that assigns to every object of AMI an element of the same kind. In this paper we develop the theory of AMI. Some properties of AMI are introduced ensuring it to have some properties of real computers: \begin{description} \item{ - }a von Neumann AMI, in which only addresses to instruction locations are stored in the program counter, \item{ - }data oriented, those in which instructions cannot be stored in data locations, \item{ - }halting, in which the execution of the halt instruction is the identity mapping of the states of an AMI, \item{ - }steady programmed, the condition in which the contents of the instruction locations do not change during execution, \item{ - }definite, a property in which only instructions may be stored in instruction locations. \end{description} We present an example of AMI called a Small Concrete Model which has been constructed in [13]. The Small Concrete Model has only one kind of data: integers and a set of instructions, small but sufficient to cope with integers.

MML Identifier: AMI_1

The terminology and notation used in this paper have been introduced in the following articles [15] [8] [17] [16] [2] [18] [5] [6] [11] [1] [9] [14] [10] [3] [4] [7]