超高速非同期式システムのための設計および検証ツールに関する研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 12680334
• Research Institution: National Institute of Informatics
• Principal Investigator: 米田 友洋 国立情報学研究所, 情報基盤研究系, 教授 (30182851)
• Keywords: 非同期式回路 / 形式的検証 / 3値2線式符号 / 高位記述 / 有限幅遅延モデル / タイムペトリネット / Partial order reduction

Research Abstract

本研究の主要な目的は,3値2線式符号に基づく設計法の確立と「データパスは(ランダムデータに基づき)確率的に,制御部は網羅的に」検証を行うことで,人手による簡単化・抽象化を不要とした検証手法の開発である.昨年度は、後者を一般化したレベル指向モデルに基づく検証方式について主に検討し,そのモデルの解析にpartial order reduction手法を適用するためのアルゴリズムを形式的に記述した.本年度は,このアルゴリズムを本格的に実装し,いくつかのベンチマーク回路に適用して効率を評価した.その結果,partial order reduction手法の効果は非常に大きいことを確認するとともに,レベル指向モデルを用いることにより,モデルが大幅に簡単になることがあり,そのような場合には,従来の遷移指向モデルで記述した場合よりも検証自体の高速化が図れることがわかった.また.アルゴリズムの正しさに関する証明のスケッチを得た.レベル指向モデルをpartial order reduction手法を用いて解析することは,本研究を進める上で発展的に得られた結果であり,本来の計画を越えた部分である.そのため,厳密な証明を完了するにはもう少し時間が必要である.
一方,高位仕様記述言語による仕様記述に関しては,ハードウェア記述言語であるVHDLのサブセットをレベル指向モデルに変換する変換器を作成した.また,これを用いて,非同期式プロセッサTITAC2の命令キャッシュ制御回路の一部を記述,変換し,その動作を確認した。この実装では,VHDLのサブセットを対象としたが,核となる部分は言語に大きく依存しないため,今後,他の仕様記述言語についても検討し,記述能力,可読性などを検討した上で,適当な仕様記述言語を決定し,本格的なツールとして完成させる予定である.