Formal Semantics for the Automated Derivation of Micro-Code

A semantics based scheme for use in machine-independent microprogram synthesis is described. The input to the synthesis system consists of a micro-instruction set processor model and requirement specifications. Validity and transformation rules which are an integral part of the system are used in an attempt to prove the existence of a microprogram satisfying the requirements and if feasible such a microprogram can be extracted directly from the proof. The primary goal of this paper is to describe a system of validity and transformation rules for use in such a synthesis system.