| 研究概要 |
本年度は,以下の三種類の研究を行った。
1.割り込みによるHW-SW間の通信を行う設計に対する形式的検証手法を実現するための調査を行い、検証方法の検討を行った。割り込みは任意のタイミングで発生し得るため、単純に扱うと計算量が増大してしまう。そこで、割り込み許可/禁止信号の解析により、割り込みが発生しうるタイミングを得る。さらに、割り込みにより送受信されるデータの依存を解析する事で、割り込みのタイミングが異なってもデータフローが同一である状況は単一事象として扱う。以上の工夫により状態数が削減され、実際的な設計が検証可能となると考えられる。
2.大規模な設計に対する等価性検証では、計算量が設計規模や制御の複雑度などに対して指数的であるという問題がある。そこで、設計に対して等価な変換を適用して、同一の正規形に変換されれば二つの設計は等価であるという判定を行う手法を提案する。動作の解析を行わないため、高速な判定が可能であると考えられる。現在、本手法の項書き換えシステムへの帰着に向けて、項書き換えシステムの調査が完了している。
3.既存の検証ツール開発では、入力となる設計記述言語の種類や抽象度が多様化しているという問題点がある。さらに、レジスタ転送レベル以上の高位設計の検証において重要であるワードレベルに対応する有用な中間表現は現時点で乏しい。そこで本研究では、FSMDと、システム依存グラフをベースとした効率的な中間表現を提案する。システム依存グラフを探索することにより検証に必要な情報を効率的に抽出でき、全ての設計をFSMDに変換することにより、入力言語に依存しない検証システムを開発可能となる。現在、提案する中間表現を実現するためのライブラリのうちFSMD部分の開発が完了している。
|
