|
類似度に基づく等価検証を行うシステムの実現に向けて、C言語から等価論理の式を生成するシステムおよびその等価論理式を時間展開するシステムの構築を行った。また、先に作成したVerilogを等価論理の式に変換して時間展開するシステムと合わせて、ハードウェア機能のC言語記述とVerilog記述し、それらが等価であるかどうかの検証を行うシステムのプロトタイプを構築した。類似度については、等価論理式の枠内での導入を行い、絶対値の差に基づく手法、現在の変数値との差に基づく手法の検討を行った。生成された等価論理式に対し、公開されている等価論理判定システムであるCVCLやYICESを適用し、本手法の有効性の確認を行った。また大規模な問題への適用のため、等価論理式をSATの問題に帰着して解く手法について研究を行い、変数間の等価性の推移的閉方を効率化する手法の検討を行った。さらに具体的なハードウェアヘの適用として、マルチスレッディングプロセッサの等価性判定手法の検討を行い、6スレッドが同時に実行されるマルチスレッディングプロセッサの命令発効を行う論理の設計と検証、および実設計で要求の高い演算器の最適化と等価性判定についても研究を行った。マルチスレッディングプロセッサの検証では、等価論理と同時にプロトタイピング字のアサーション検証手法も適用した。また演算器の検証では、加算器のプレフィックスグラフの最適化と等価性検証という問題に取り組み、最長経路を無効化する回路の追加により、素子数とのトレードオフを考えながら最適化を行う手法を提案した。
|
