| 講演名 | 2007-01-18 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般) 藤田 裕久, 濱田 雅彦, 谷本 匡亮, 中田 明夫, 東野 輝夫, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ハードウェアには配線遅延があるためクロック周波数の向上に限界がある.そこで,実行時間削減を目的としてクロックサイクルを消費しない即時通信がしばしば用いられる.そのような通信を行うサイクル精度動作記述には,組み合わせ回路としての閉路が発生することに起因する値の発振や発散の可能性といった難しさがある.そこで,本論文ではwireによる即時通信を行うサイクル精度動作記述モジュール群に発振や発散の問題が生じるか否か等を,モデル検査によって検証する手法を提案する.実験では上述した問題の発生を含んだ簡単なテストケース群に対して提案手法を適用し,その有効性を確認した. |
| 抄録(英) | Wiring delay imposes a limitation on increase of clock frequency. Therefore, instantaneous communications consuming no clock cycles are sometimes used. Cycle accurate behavior models allowing such communications have a problem of oscillation and divergence in variable values caused by combinational loops. In this paper, we propose a model checking method of cycle accurate behavior models including instantaneous communications of wire. Proposed method can detect the occurrence of oscillation, divergence and other problems like access conflict. In the experiments, we confirmed the effectiveness of our method using several simple test cases. |
| キーワード(和) | 設計検証 / サイクル精度 / 即時通信 / 組み合わせ閉路 / モデル検査 |
| キーワード(英) | instantaneous communication / constructive analysis / combinational loops / cycle accurate behavior model / model checking |
| 資料番号 | VLD2006-98,CPSY2006-69,RECONF2006-69 |
| 発行日 |
| 研究会情報 | |
| 研究会 | RECONF |
|---|---|
| 開催期間 | 2007/1/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Reconfigurable Systems (RECONF) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Model Checking of Cycle Accurate Hardware Behavior Models with Instantaneous Communication |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 設計検証 / instantaneous communication |
| キーワード(2)（和/英） | サイクル精度 / constructive analysis |
| キーワード(3)（和/英） | 即時通信 / combinational loops |
| キーワード(4)（和/英） | 組み合わせ閉路 / cycle accurate behavior model |
| キーワード(5)（和/英） | モデル検査 / model checking |
| 第 1 著者 氏名（和/英） | 藤田 裕久 / Hirohisa FUJITA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 濱田 雅彦 / Masahiko HAMADA |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 谷本 匡亮 / Tadaaki TANIMOTO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Information Science and Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 中田 明夫 / Akio NAKATA |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Information Science and Technology, Osaka University |
| 第 5 著者 氏名（和/英） | 東野 輝夫 / Teruo HIGASHINO |
| 第 5 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Dept. of Information Science and Technology, Osaka University |
| 発表年月日 | 2007-01-18 |
| 資料番号 | VLD2006-98,CPSY2006-69,RECONF2006-69 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 458 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |