動作レベルおよびレジスタ転送レベルのハードウェア記述に対する形式的検証手法の研究

点击翻译按钮获取中文摘要

本研究課題では,動作レベルの記述を扱うことができるフォーマル検証技術の確立を目指している.この背景には,今後,設計生産性向上のため,動作レベルからの設計および自動合成が広く利用されるようになるであろうという予測がある.具体的な研究テーマとして,記号シミュレーションを利用した,動作レベル/レジスタ転送レベルの検証手法に関して,次の点を目標とした.特にCプログラムで数百行相当,レジスタ転送レベルでの実行ステップ数が数万サイクルの設計を目標とした.1.記号シミュレーションに基づく等価性判定アルゴリズムの省メモリ化/高速化.2.プロパティ・チェック手法の開発.3.第1階述語論理の部分クラスに対する恒真性判定アルゴリズムの高速化.平成13年度は,3.のアルゴリズムの作成およびそれに基づく1.のアルゴリズムを実装して評価を行った.3.のアルゴリズムに対して「記号関数表」,1.のアルゴリズムに対して「強制同期」と名付けたヒューリスティクを用いることにより,研究開始前に作成していたプロトタイプに比べ,高速化と省メモリ化に成功した.具体的には,1GBのメモリを要し,24分かかった例題(DSPの設計例)を,386MBのメモリで4分で検証することができるようになった他,制御構造に2重ループを含むような例題(レジスタ転送レベルの実行サイクル数が37500サイクル)についても,検証が可能となった(検証時間は8時間20分).プロトタイプのシミュレータでは,必要記憶容量が大きすぎ,この例題を扱うことはできなかった.2.のプロパティチェックアルゴリズムについては,上記の記号シミュレータをベースにして,ユーザが与えた有限サイクル数分について,プロパティチェックを行うアルゴリズムを開発した.また,これを実装して,簡単な例題への適用を試みた.当初の計画通り,第一階述語論理の部分クラスに対する記号シミュレーションを,より大きな設計例へ適用できるようになりつつある.しかしながら,この部分クラスの論理のセマンティクスでは,本来等価となるべき例でも等価にならない場合がある.現在,この問題に対する解決策の1つとして,限定的な等式制約のもとでの等価性判定について検討を進めている.