PRL Seminars

Verifying a pipelined circuit is more difficult than a non-pipelined circuit, because multiple computations are active simultaneously, and computations are dispersed over a number of clock cycles and functional units. This introduces several complications, including contention for resources between transactions, which can lead to problems in termination and interference between transactions. These difficulties must be resolved before we can begin to verify the correctness of the datapath of the pipeline.

We have formally defined what it means for a pipeline to be correct. We developed a framework that organizes the verification into four separate and largely independent tasks. Each of these tasks is represented by a parameter to the framework that is instantiated for individual pipelines. We have identified specifications that choices for the parameters to the framework must satisfy, and have proved that any pipeline that satisfies these specifications will guarantee termination and freedom from interference for transactions. These conditions are sufficient to replace a proof about the input/output behavior of the implementation with a proof about a combinational logic model of the datapath of the pipeline. The conditions are very general and support complex features found in state-of-the-art microprocessors, such as super-scalar issue, out-of-order completion, and any mixture of data-stationary, time-stationary or data-dependent control.

The talk will presume only a cursory familiarity with hardware design and verification.