The formal specification of instruction set processors and the derivation of instruction schedulers
E. Harcourt · 1995
We present two techniques for formally specifying an instruction set processor at the programmer's view--the architecture view and the timing view. From the timing specification we show how to derive an instruction scheduler for the processor. One technique addresses architecture specification, that is, the information required to write correct programs. At the architectural level we present a functional semantics that captures the property that instructions are functions from processor state to processor state. The second specification technique addresses the programmer's view of the timing of the processor, that is, the needed information required to write temporally efficient programs. We present a technique for formally describing, at a high-level, the timing properties of pipelined, superscalar processors. We illustrate the technique by specifying and simulating a hypothetical processor that includes many features of commercial processors including delayed loads and branches, interlocked floating-point instructions, and multiple instruction issue. As our mathematical formalism we use SCCS, a synchronous process algebra designed for specifying timed, concurrent systems. Putting our specification to use, we show how to construct an instruction-scheduler from the specification by deriving appropriate parameters needed for instruction scheduling. These parameters include instruction latencies, illegal instruction combinations, resource constraints, and instructions that may be issued in parallel.