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_1,--,stg_n such that the stages stg_c,--,stg_n are so-called "inorder pipeline" and changes the execution order of instructions within the stages of stg_1,--,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(1). We used a verifier having a decision procedure for Presburger sentences. The total CPU time spent in the proof was about 8 hours.