Formal Verification of Bypassed Processor Pipelines

With the development and application of pipeline technique in processor, the verification of pipeline designs is becoming important in academies and industries. This paper presents a method to model and check the correctness of pipeline with bypass configuration at instruction level. This method is based on model checking, a method of formal verification. This method not only suits for the complete bypass design, but also can be used to check the validation of partial bypass configuration. The properties a bypassed design should satisfy are also provided. And the abstracted model can be verified automatically by using NuSMV, which is a tool used for model checking. If the properties cannot be satisfied, a counterexample is created to help correct the design or the model.