| 研究概要 |
近年のハードウェア設計では,設計検証が設計工程の半分以上を占めるようになっている.設計および検証効率を改善するため,ハードウェア設計をCやSystemCといった高位の言語で記述するアプローチが実用的にも取り入れられるようになってきている.本研究は,C言語などで記述された高位ハードウェアの設計に対するフォーマル検証手法,とくにモデル検査の手法を開発することを目的としている.本年度は交付申請書に記した通り,次の研究を行った.
1.同値制約規則の動的自動抽出の基礎実験とアルゴリズムの検討
2.複数の充足可能性判定器を組み合わせたモデル検査アルゴリズムの検討
1.については,基礎実験として2つのプログラムに対して,ランダムシミュレーションと等価性判定を組み合わせることにより,同値制約を抽出するアルゴリズムを開発・実装した.Parcorフィルタや,ADPCM変換などのプログラムに対して,人為的な変更を加えて,実装したプログラムを適用し,確かに所望の同値制約を取り出すことができた.自動抽出の手間を含めても,従来のプール関数レベルでのフォーマル検証に比べて,特に設計規模が大きくなった場合に高速に検証が行えることも確認した.
2.については,C言語で書かれたプログラムに対して限量子を含まない等号付き第1階述語論理と線形算術式を組み合わせてフォーマル検証を行うアルゴリズムを検討した.現在,実装に取りかかっている.
上記の成果をふまえて,次年度は特に2.のアルゴリズムの実装を中心に研究を進める予定である.
|
