Getting the interlock logic that controls the pipeline flow of a pipelined design, e.g. a microprocessor, right first time is an important prerequisite for maximising pipeline throughput. Performance bugs in this area are often due to unnecessary pipeline stalls. Unnecessary pipeline stalls can only be eliminated when they can be distinguished from those stalls which are necessary to preserve functional correctness.
I will show how a maximum pipeline performance specification can be derived from a complete functional specification of the pipeline control logic. The specifications can be developed early in the design process and can support several design stages, including testing, property checking and even code generation.
This is joint work with Geoff Barrett, Broadcom Corporation.