THE FORMAL SPECIFICATION OF A MICROPROCESSOR INSTRUCTION SET

Abstract

The specification language Z is used to define a microprocessor based system in a formal notation. The Motorola 6800 8-bit microprocessor is chosen as an example. Its simplicity allows the entire instruction set to be covered. Memory configuration and interrupts are also included. The use of a formal description language allows the possibility of verification of the instruction set. Additionally the use of Z combined with informal text is sufficiently readable for the specification to be used for documentation purposes.