2009 Fiscal Year Annual Research Report
高位ハードウェア設計記述に対するモデル検査手法の研究
| Project/Area Number |
19500043
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
浜口 清治 Osaka University, 大学院・情報科学研究科, 准教授 (80238055)
|
|---|
| Keywords | 設計検証 / フォーマル検証 / 第一階述語論理 / モデル検査 / 高位ハードウェア検証 |
|---|
| Research Abstract |
近年のハードウェア設計では,設計検証が設計工程の半分以上を占めるようになっている.近年,設計および検証効率を改善するため,ハードウェア設計を高位の言語で記述するアプローチが実用的にも取り入れられるようになってきているが,とくに,高位のハードウェア記述に対するフォーマル検証手法については,必ずしも十分な研究が行われているとは言えない.本研究では,C言語などで記述された高位ハードウェアの設計に対するフォーマル検証手法,とくにモデル検査の手法を開発することを目的とする.平成21年度は特に次の点について研究を行って成果を得た.
・複数の論理体系を組み合わせた近似的モデル検査アルゴリズムの実装と評価
前年度までに得られていた複数の論理体系を組み合わせた有界モデル検査の手法と,EUF(限量子を含まない等号付き第一階述語論理)に対する近似的な非有界モデル検査の手法を融合して,さらに,利用する複数の論理体系を動的に変化させる手法を新たに導入することにより,非有界モデル検査が可能なアルゴリズムを考案・実装し,評価を行った.この手法では,当初はEUFのみで検証を行って,うまく行かなかった場合に,線形算術論理,ビットベクトル論理と順番に論理体系を切り替えて,検証の近似度をさげていく.これにより,前年度までに開発手法を含む従来手法では扱うことができなかった,信号処理プログラム(ADPCM)の例題について,現実的な時間(~250秒程度)で検証可能となることを示した.
|
