| 講演抄録／キーワード |
| 講演名 |
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ダウンロード |
|