Formal design verification for correctness of pipelined microprocessors with out-of-order instruction execution

In this paper, we propose a verification method for pipelined microprocessors with out-of-order execution. We define a class of pipelined microprocessors with out-of-order execution and give a sufficient condition that guarantees the correctness of implementation. Each microprocessor in this class has a pipeline stg₁,…,stg_n such that the stages stg_c ,…,stg_n are so-called “in-order pipeline” and changes the execution order of instructions within the stages of stg₁,…,stg_c-1. Using our method, we carried out the correctness proof of a practical 6-stage pipelined microprocessor that has a so-called scoreboard. We used a verifier having a decision procedure for Presburger sentences. The total CPU time spent in the proof was about 8 hours