| 講演名 | 1996/10/18 in-order実行パイプラインCPUの正しさの自動証明例 島谷 肇, 森岡 澄夫, 東野 輝夫, 谷口 健一, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 我々は, 命令のin-order実行のみを行うパイプラインCPUを設計する一つの手法と, それによって設計した実現の正しさを, 代数的手法を用いて自動で証明する手法を提案している. 設計では, 要求仕様から次のように段階的詳細化を行いRTレベルを得る. まずパイプラインの各ステージの動作を決め, 次にフォーワーディングやストールを行いながらそれらを重ね合わせる. 実現の正しさの証明では, 実現の各ステージごとに検証条件を求め, 代数的手法を用いてその恒真性を判定する. 実際に, 提案した手法に基づく検証支援系を作成した. 本支援系を用いて, 命令セットが11命令からなる5ステージ・パイプラインCPUの正しさの証明の一部を行うことができた. |
| 抄録(英) | 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. |
| キーワード(和) | パイプラインCPU / in-order実行 / 段階的詳細化 / 正しさの証明 / 代数的手法 / 検証支援系 |
| キーワード(英) | Pipelined CPU / In-order execution / Step-wise refinement / Correctness proof / Algebraic method / Verification support system |
| 資料番号 | VLD96-62 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 1996/10/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | in-order実行パイプラインCPUの正しさの自動証明例 |
| サブタイトル（和） | |
| タイトル（英） | Automatic Correctness Proof of a Pipelined CPU with In-Order Exection |
| サブタイトル（和） | |
| キーワード(1)（和/英） | パイプラインCPU / Pipelined CPU |
| キーワード(2)（和/英） | in-order実行 / In-order execution |
| キーワード(3)（和/英） | 段階的詳細化 / Step-wise refinement |
| キーワード(4)（和/英） | 正しさの証明 / Correctness proof |
| キーワード(5)（和/英） | 代数的手法 / Algebraic method |
| キーワード(6)（和/英） | 検証支援系 / Verification support system |
| 第 1 著者 氏名（和/英） | 島谷 肇 / Hajime SHIMATANI |
| 第 1 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 森岡 澄夫 / Sumio MORIOKA |
| 第 2 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 東野 輝夫 / Teruo HIGASHINO |
| 第 3 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 第 4 著者 氏名（和/英） | 谷口 健一 / Kenichi TANIGUCHI |
| 第 4 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 発表年月日 | 1996/10/18 |
| 資料番号 | VLD96-62 |
| 巻番号（vol） | vol.96 |
| 号番号（no） | 299 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |