| 講演名 | 1997/3/6 レジスタ転送レベル論理回路の設計検証のための回路縮小法について 坂手 孝規, 木村 晋二, 渡邉 勝正, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では、レジスタ転送レベルのハードウェア記述を縮小して設計検証に用いる手法を提案する。大規模な回路の形式的な検証は膨大な計算時間や領域を必要とするので、現状では人手で回路を縮小して検証する手法がとられている。しかし、人手による縮小過程には誤りが含まれている可能性があるので完全に正しいとはいえない。本稿で提案する縮小法は、元の回路からレジスタ代入関係を抽出して縮小回路を自動的に生成する方法である。この縮小法は、縮小した回路の検証結果が元の回路の検証結果と等価であることが証明できるので、大規模な論理回路のレジスタ代入関係に基づく形式的な検証が可能となる。またこの手法を、パイプラインプロセッサに適用して、データ依存に関する検証例を示す。 |
| 抄録(英) | This paper shows a reduction method of register transfer level circuits for symbolic execution based formal verification. On the symbolic execution, the nodes of BDD's may blow up, and we should make a reduced verification model by hand. The method proposed in the paper reduces circuits using the equivalence relation, and is proved to produce the same verification result. The reduced model of a pipeline processor is also shown and the data dependency is verified using the reduced model. |
| キーワード(和) | レジスタ転送レベル回路 / 縮小回路モデル / ハードウェア記述言語 / 記号実行 / 二分決定グラフ / パイプライン動作の検証 |
| キーワード(英) | Register Transfer Level Circuit / Reduced Verification Model / Hardware Description Language / Symbolic Execution / Binary Decision Diagram / Verification of Pipeline Behavior |
| 資料番号 | VLD96-91,ICD96-201 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 1997/3/6(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | レジスタ転送レベル論理回路の設計検証のための回路縮小法について |
| サブタイトル（和） | |
| タイトル（英） | A Reduction Method of Register Transfer Level Logic Circuits for Design Verification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | レジスタ転送レベル回路 / Register Transfer Level Circuit |
| キーワード(2)（和/英） | 縮小回路モデル / Reduced Verification Model |
| キーワード(3)（和/英） | ハードウェア記述言語 / Hardware Description Language |
| キーワード(4)（和/英） | 記号実行 / Symbolic Execution |
| キーワード(5)（和/英） | 二分決定グラフ / Binary Decision Diagram |
| キーワード(6)（和/英） | パイプライン動作の検証 / Verification of Pipeline Behavior |
| 第 1 著者 氏名（和/英） | 坂手 孝規 / Takanori Sakate |
| 第 1 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Nara Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | 木村 晋二 / Shinji Kimura |
| 第 2 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Nara Institute of Science and Technology |
| 第 3 著者 氏名（和/英） | 渡邉 勝正 / Katsumasa Watanabe |
| 第 3 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Nara Institute of Science and Technology |
| 発表年月日 | 1997/3/6 |
| 資料番号 | VLD96-91,ICD96-201 |
| 巻番号（vol） | vol.96 |
| 号番号（no） | 555 |
| ページ範囲 | pp.- |
| ページ数 | 7 |
| 発行日 | |