|
ハードウェアの高位レベルの等価検証手法の確立を目的とし、類似度を考慮した等価論理に基づく等価検証システムの研究を行った。等価論理は、変数の等価性のみに着目した論理体系で、他の論理との組合せで高い検証機能を持つことが知られている。まず、Verilog記述から等価論理の式を生成するシステムと、C言語記述から等価論理の式を生成するシステム、およびこれらの変換された等価論理式を時間展開するシステムのプロトタイプの構築を行った。生成された時間展開後の等価論理式に対し、公開されている等価論理判定システムであるCVCLやYICESを適用し、本手法の正当性と有効性の確認を行った。また現状の等価論理判定手法が時間展開に対して指数的な計算量を必要とすることが実験的に確認できたため、等価論理式をSATの問題に帰着して解く手法について研究を行い、変数間の等価性の推移的閉方を効率化する手法の検討を行った。類似度については、等価論理式の枠内での導入を行い、絶対値の差に基づく手法、現在の変数値との差に基づく手法の検討を行った。またハードウェア設計における浮動小数点数の固定小数点数への変換時の誤差と類似度の関係についても研究を行い、固定小数点数のビット数の最適化手法を提案した。さらに具体的なハードウェアへの適用として、マルチスレッディングプロセッサの等価性検証、加算のプレフィックスグラフの最適化と等価性検証、プロトタイピングを用いた等価検証の高速化とプロトタイピング検証におけるアサーション検証手法の高速化について研究を行った。
|
