| 講演抄録／キーワード |
| 講演名 |
2007-01-18 11:25
即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法
○藤田裕久・濱田雅彦・谷本匡亮・中田明夫・東野輝夫（阪大） |
| 抄録 |
（和） |
ハードウェアには配線遅延があるため
クロック周波数の向上に限界がある．そこで，
実行時間削減を目的として
クロックサイクルを消費しない即時通信が
しばしば用いられる．
そのような通信を行うサイクル精度動作記述には，
組み合わせ回路としての閉路が発生することに起因する
値の発振や発散の可能性といった難しさがある．
そこで，本論文では
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 / cycle accurate behavior model / model checking / / / / |
| 文献情報 |
信学技報, vol. 106, pp. 25-30, 2007年1月. |
| 資料番号 |
|
| 発行日 |
2007-01-11 (VLD, CPSY, RECONF) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|
| 研究会情報 |
| 研究会 |
VLD CPSY RECONF IPSJ-SLDM |
| 開催期間 |
2007-01-17 - 2007-01-18 |
| 開催地（和） |
慶応大学（日吉） |
| 開催地（英） |
Keio Univ. Hiyoshi Campus |
| テーマ（和） |
FPGAとその応用および一般 |
| テーマ（英） |
FPGA and its Application, etc. |
| 講演論文情報の詳細 |
| 申込み研究会 |
IPSJ-SLDM |
| 会議コード |
2007-01-VLD-CPSY-RECONF-IPSJ-SLDM |
| 本文の言語 |
日本語 |
| タイトル（和） |
即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法 |
| サブタイトル（和） |
|
| タイトル（英） |
Model Checking of Cycle Accurate Hardware Behavior Models with Instantaneous Communication |
| サブタイトル（英） |
|
| キーワード(1)（和/英） |
設計検証 / instantaneous communication |
| キーワード(2)（和/英） |
サイクル精度 / constructive analysis |
| キーワード(3)（和/英） |
即時通信 / cycle accurate behavior model |
| キーワード(4)（和/英） |
組み合わせ閉路 / model checking |
| キーワード(5)（和/英） |
モデル検査 / |
| キーワード(6)（和/英） |
/ |
| キーワード(7)（和/英） |
/ |
| キーワード(8)（和/英） |
/ |
| 第1著者 氏名（和/英/ヨミ） |
藤田 裕久 / Hirohisa Fujita / フジタ ヒロヒサ |
| 第1著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） |
濱田 雅彦 / Masahiko Hamada / ハマダ マサヒコ |
| 第2著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第3著者 氏名（和/英/ヨミ） |
谷本 匡亮 / Tadaaki Tanimoto / タニモト タダアキ |
| 第3著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第4著者 氏名（和/英/ヨミ） |
中田 明夫 / Akio Nakata / ナカタ アキオ |
| 第4著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第5著者 氏名（和/英/ヨミ） |
東野 輝夫 / Teruo Higashino / ヒガシノ テルオ |
| 第5著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第6著者 氏名（和/英/ヨミ） |
/ / |
| 第6著者 所属（和/英） |
(略称： )
(略称： ) |
| 第7著者 氏名（和/英/ヨミ） |
/ / |
| 第7著者 所属（和/英） |
(略称： )
(略称： ) |
| 第8著者 氏名（和/英/ヨミ） |
/ / |
| 第8著者 所属（和/英） |
(略称： )
(略称： ) |
| 第9著者 氏名（和/英/ヨミ） |
/ / |
| 第9著者 所属（和/英） |
(略称： )
(略称： ) |
| 第10著者 氏名（和/英/ヨミ） |
/ / |
| 第10著者 所属（和/英） |
(略称： )
(略称： ) |
| 第11著者 氏名（和/英/ヨミ） |
/ / |
| 第11著者 所属（和/英） |
(略称： )
(略称： ) |
| 第12著者 氏名（和/英/ヨミ） |
/ / |
| 第12著者 所属（和/英） |
(略称： )
(略称： ) |
| 第13著者 氏名（和/英/ヨミ） |
/ / |
| 第13著者 所属（和/英） |
(略称： )
(略称： ) |
| 第14著者 氏名（和/英/ヨミ） |
/ / |
| 第14著者 所属（和/英） |
(略称： )
(略称： ) |
| 第15著者 氏名（和/英/ヨミ） |
/ / |
| 第15著者 所属（和/英） |
(略称： )
(略称： ) |
| 第16著者 氏名（和/英/ヨミ） |
/ / |
| 第16著者 所属（和/英） |
(略称： )
(略称： ) |
| 第17著者 氏名（和/英/ヨミ） |
/ / |
| 第17著者 所属（和/英） |
(略称： )
(略称： ) |
| 第18著者 氏名（和/英/ヨミ） |
/ / |
| 第18著者 所属（和/英） |
(略称： )
(略称： ) |
| 第19著者 氏名（和/英/ヨミ） |
/ / |
| 第19著者 所属（和/英） |
(略称： )
(略称： ) |
| 第20著者 氏名（和/英/ヨミ） |
/ / |
| 第20著者 所属（和/英） |
(略称： )
(略称： ) |
| 第21著者 氏名（和/英/ヨミ） |
/ / |
| 第21著者 所属（和/英） |
(略称： )
(略称： ) |
| 第22著者 氏名（和/英/ヨミ） |
/ / |
| 第22著者 所属（和/英） |
(略称： )
(略称： ) |
| 第23著者 氏名（和/英/ヨミ） |
/ / |
| 第23著者 所属（和/英） |
(略称： )
(略称： ) |
| 第24著者 氏名（和/英/ヨミ） |
/ / |
| 第24著者 所属（和/英） |
(略称： )
(略称： ) |
| 第25著者 氏名（和/英/ヨミ） |
/ / |
| 第25著者 所属（和/英） |
(略称： )
(略称： ) |
| 第26著者 氏名（和/英/ヨミ） |
/ / |
| 第26著者 所属（和/英） |
(略称： )
(略称： ) |
| 第27著者 氏名（和/英/ヨミ） |
/ / |
| 第27著者 所属（和/英） |
(略称： )
(略称： ) |
| 第28著者 氏名（和/英/ヨミ） |
/ / |
| 第28著者 所属（和/英） |
(略称： )
(略称： ) |
| 第29著者 氏名（和/英/ヨミ） |
/ / |
| 第29著者 所属（和/英） |
(略称： )
(略称： ) |
| 第30著者 氏名（和/英/ヨミ） |
/ / |
| 第30著者 所属（和/英） |
(略称： )
(略称： ) |
| 第31著者 氏名（和/英/ヨミ） |
/ / |
| 第31著者 所属（和/英） |
(略称： )
(略称： ) |
| 第32著者 氏名（和/英/ヨミ） |
/ / |
| 第32著者 所属（和/英） |
(略称： )
(略称： ) |
| 第33著者 氏名（和/英/ヨミ） |
/ / |
| 第33著者 所属（和/英） |
(略称： )
(略称： ) |
| 第34著者 氏名（和/英/ヨミ） |
/ / |
| 第34著者 所属（和/英） |
(略称： )
(略称： ) |
| 第35著者 氏名（和/英/ヨミ） |
/ / |
| 第35著者 所属（和/英） |
(略称： )
(略称： ) |
| 第36著者 氏名（和/英/ヨミ） |
/ / |
| 第36著者 所属（和/英） |
(略称： )
(略称： ) |
| 講演者 |
第1著者 |
| 発表日時 |
2007-01-18 11:25:00 |
| 発表時間 |
25分 |
| 申込先研究会 |
IPSJ-SLDM |
| 資料番号 |
VLD2006-98, CPSY2006-69, RECONF2006-69 |
| 巻番号（vol） |
vol.106 |
| 号番号（no） |
no.454(VLD), no.456(CPSY), no.458(RECONF) |
| ページ範囲 |
pp.25-30 |
| ページ数 |
6 |
| 発行日 |
2007-01-11 (VLD, CPSY, RECONF) |