High level timing specification of instruction-level parallel processors
Ed Harcourt, Jon Mauney, Todd A. Cook · NCSU Libraries Repository (North Carolina State University Libraries) · 1993
In modern instruction set processors, the temporal and concurrent properties of the instructions are often visible to the user of the processor.To use the processor as eciently as possible, the user needs this information.Consequently, this instruction-level parallelism should be included in any behavioral processor speci cation.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 oating-point instructions, and multiple instruction issue.As our mathematical formalism we use SCCS, a synchronous process algebra designed for specifying timed, concurrent systems.Formal speci cations are a fundemental and logical starting point for solving a variety of problems, including: veri cation, simulation, synthesis, and precise documentation.In addition, a formal speci cation aids in the design process as it requires a designer to rigorously and thoughtfully plan the design in a structured manner.