Achieving maximum performance: a method for the verification of interlocked pipeline control logic

Getting the interlock logic which controls pipeline flow correct is an important prerequisite for maximising pipeline performance. Unnecessary pipeline stalls can only be eliminated when they can be distinguished from those stalls which are necessary to preserve functional correctness. Typically, designers know when these necessary stalls should occur.We propose a method for deriving a maximum pipeline performance specification from a complete functional specification of the pipeline control logic. The performance specification can be used to generate simulation testbench assertions. On the other hand, the specification can serve as a basis for formal property checking. The most promising aspect of our work is, however, the potential to synthesise the actual control logic from its formal description.