In contrast, attempts to reduce verification effort and increase confidence in correctness tend to limit the exploration of the design space. One potential method for mitigating the tension between verifiability and the other metrics is to formalize the microarchitectural level of description. Just as the register-transfer level serves as an abstraction of the switch level and the switch level abstracts the analog level, the microarchitectural level should facilitate both design and verification by hiding irrelevant detail of the lower levels.
Pipelines are a pervasive and complex feature of the microarchitectural level.
Despite an almost endless variety of implementations, they have a uniform correctness criteria and some common design patterns. These features make pipelines an excellent candidate for beginning the formalization of the microarchitectural level. In this talk I will illustrate some of the complexities found in high-performance pipelines and present a compositional theory of correctness for pipelined circuits. I will then discuss lessons learned in developing an industrially successful formal verification system for the register-transfer level and how these lessons can be applied to pipelines at the microarchitectural level.