in-order 実行パイプラインCPUの正しさの自動証明例
書誌事項
- タイトル別名
-
- Automatic Correctness Proof of a Pipelined CPU with In-Order Exection
この論文をさがす
説明
我々は, 命令のin-order実行のみを行うパイプラインCPUを設計する一つの手法と, それによって設計した実現の正しさを, 代数的手法を用いて自動で証明する手法を提案している. 設計では, 要求仕様から次のように段階的詳細化を行いRTレベルを得る. まずパイプラインの各ステージの動作を決め, 次にフォーワーディングやストールを行いながらそれらを重ね合わせる. 実現の正しさの証明では, 実現の各ステージごとに検証条件を求め, 代数的手法を用いてその恒真性を判定する. 実際に, 提案した手法に基づく検証支援系を作成した. 本支援系を用いて, 命令セットが11命令からなる5ステージ・パイプラインCPUの正しさの証明の一部を行うことができた.
収録刊行物
-
- 電子情報通信学会技術研究報告. VLD, VLSI設計技術
-
電子情報通信学会技術研究報告. VLD, VLSI設計技術 96 (299), 57-64, 1996-10-18
一般社団法人電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1573668927129435648
-
- NII論文ID
- 110003294400
-
- NII書誌ID
- AN10013323
-
- 本文言語コード
- ja
-
- データソース種別
-
- CiNii Articles