Automatic Correctness Proof of a Pipelined CPU with In-Order Exection

7 References
  • SHIMATANI Hajime
    Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
  • MORIOKA Sumio
    Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
  • HIGASHINO Teruo
    Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
  • TANIGUCHI Kenichi
    Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University

Bibliographic Information

Other Title
  • in-order 実行パイプラインCPUの正しさの自動証明例

Search this article

Description

We have proposed a design and automatic proof method for pipelined CPUs with in-order execution. In a design, we carry out the following step-wise refinement to obtain a RT level. First we decide an action of each pipeline stage and arrange those stages in an order, and next pile up those actions with forwarding and stalling introduced. At the correctness proof of a realization, we check that for each pipiline stage in a realization, a verification condition holds using our algebraic methods. We made the verification support system based on the above method, and partly carried out the correctness proof of a 5-stage pipelined CPU, whose instruction set is composed of 11 instructions.

Journal

  • Technical report of IEICE. VLD

    Technical report of IEICE. VLD 96 (299), 57-64, 1996-10-18

    The Institute of Electronics, Information and Communication Engineers

References(7)*help

See more

Keywords

Details 詳細情報について

  • CRID
    1573668927129435648
  • NII Article ID
    110003294400
  • NII Book ID
    AN10013323
  • Text Lang
    ja
  • Data Source
    • CiNii Articles

Report a problem

Back to top