Formal Design Verification for Correctness of Pipelined Microprocessors with Out-of-order Instruction Execution

Abstract — 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; : : : ; st