We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This definition separates the correctness criteria associated with the pipelining aspects of a design from the functional relationship between input and output transactions. Using this definition, we developed and formally verified a technique that divides the verification of a pipeline into two separate tasks: proving that the pipelining circuitry meets the pipelining correctness criteria and that the datapath and control circuitry meet the functional specification. The first proof is data independent (except for pipelines that use data-dependent control). The second proof is purely combinational: there is no notion of time and each possible input transaction can be dealt with independently. In addition, we have created a framework that structures and simplifies the proof of the pipelining circuitry.

Original document

The different versions of the original document can be found in:

Back to Top

Document information

Published on 01/01/2012

Volume 2012, 2012
DOI: 10.1007/3-540-59047-1_40
Licence: CC BY-NC-SA license

Document Score


Views 1
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?