| 研究概要 |
近年のハードウェア設計では,設計検証が設計工程の半分以上を占めるようになっている.近年,設計および検証効率を改善するため,ハードウェア設計を高位の言語で記述するアプローチが実用的にも取り入れられるようになってきているが,とくに,高位のハードウェア記述に対するフォーマル検証手法については,必ずしも十分な研究が行われているとは言えない.本研究では,C言語などで記述された高位ハードウェアの設計に対するフォーマル検証手法,とくにモデル検査の手法を開発することを目的とする.平成20年度は特に次の2点について研究を行って成果を得た.
1.複数の充足可能性判定を組み合わせたモデル検査アルゴリズムの実装
2.実用的な例の作成の開始
1.については,線形算術論理と限量子を含まない等号付き第1階述語論理を組み合わせたモデル検査アルゴリズムを実装した.この実装では記述力を制限したCで書かれたプログラムを入力とし,それぞれの論理体系で表現できる部分を切り分けて,論理式への変換を行う次に充足可能性判定を行うことにより,記述中に埋め込まれ条件(アサーション)を検証する.いくつかの信号処理プログラムに適用した結果,代表的なモデル検査ツールであるCBMCでは計算量的に取り扱うことができず,かつ,上記の2つの論理体系をそれぞれ単独で用いたのでは,理論上取り扱うことができない例題を扱うことができた.
2.についてもparcorフィルタプログラム,離散コサイン変換プログラムなど信号処理プログラムを中心に作業を進めている.
|
