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{c},..., stg{n} are so-called "in-order 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. We use a verifier having a decision procedure for Presburger sentences. The total CPU time spent in the proof was about 8 hours.