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/sub 1/,...,stg/sub n/ such that the stages stg/sub c/,...,stg/sub n/ are so-called "in-order pipeline" and changes the execution order of instructions within the stages of stg/sub 1/,...,stg/sub 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.
展开▼
机译：在本文中，我们提出了一种针对顺序执行错误的流水线微处理器的验证方法。我们定义一类具有乱序执行的流水线微处理器，并给出充分的条件以保证实现的正确性。此类中的每个微处理器都具有流水线stg / sub 1 /，...，stg / sub n /，这样，阶段stg / sub c /，...，stg / sub n /被称为“按顺序”流水线”，并在stg / sub 1 /，...，stg / sub c-1 /阶段更改指令的执行顺序。使用我们的方法，我们对具有所谓记分板的实用6级流水线微处理器进行了正确性证明。我们使用了具有对Presburger句子进行判决的决策程序的验证程序。证明中花费的CPU总时间约为8个小时。
展开▼
