論理回路の縮約モデルの自動抽出とそれを用いた大規模論理回路の設計検証に関する研究

本研究では、論理回路の縮約モデルの抽出と、それを用いた大規模論理回路の検証に関する研究を行った。まず、縮約モデルを用いた検証手法に関する調査研究を行なった。つぎに現在多くの論理設計検証手法で用いられている二分決定グラフ(Binary Decision Diagram、BDD)について研究を行なった。特に回路の内部の適当な論理ゲートの出力を変数として扱ってBDDを小さくするとともに、相異なる内部変数を持つ二つの回路の等価性判定を行なう手法の研究を行なった。等価性判定では、一方の回路の内部変数を他方の回路の内部変数へ多項式時間で変換する手法を新たに開発して用いた。第二に、乗算など算術演算回路で二分決定グラフの節点爆発を抑制する手法を提案した。これは数の剰余数表現に基づく手法で、算術演算回路の入力が二進数に対応づけられているという性質を用い、二分決定グラフの節点数を入力変数の数の多項式で限定する。限定された結果のBDDを剰余BDD(Residue BDD)と呼ぶ。検証では、回路を複数の法について個別に検証する。剰余数表現で知られているように、もとの関数の剰余の組で、もとの関数を完全に表せるので、検証においても各剰余毎の検証で良い。研究ではまず剰余BDDを組み合わせ回路の検証に適用し、ある程度の効果を確認した。また、乗算器など算術演算回路を含む順序回路の検証への適用についても研究を行なった。第三に、プロセッサの検証などで重要な、回路の構造に基づく縮約手法の研究を行ない、論理回路をグラフと見て、構造が等しい部分を縮約するという手法の研究を行なった。さらに、時相論理に基づく仕様記述法について研究を行ない、仕様記述から仕様記述に関係のない回路部分を縮約する手法の研究を行なった。

本研究では、論理回路の縮約モデルの抽出と、それを用いた大規模論理回路の検証に関する研究を行った。まず、縮約モデルを用いた検証手法に関する調査研究を行なった。つぎに現在多くの論理設計検証手法で用いられている二分決定グラフ(Binary Decision Diagram、BDD)について研究を行なった。特に回路の内部の適当な論理ゲートの出力を変数として扱ってBDDを小さくするとともに、相異なる内部変数を持つ二つの回路の等価性判定を行なう手法の研究を行なった。等価性判定では、一方の回路の内部変数を他方の回路の内部変数へ多項式時間で変換する手法を新たに開発して用いた。第二に、乗算など算術演算回路で二分決定グラフの節点爆発を抑制する手法を提案した。これは数の剰余数表現に基づく手法で、算術演算回路の入力が二進数に対応づけられているという性質を用い、二分決定グラフの節点数を入力変数の数の多項式で限定する。限定された結果のBDDを剰余BDD(Residue BDD)と呼ぶ。検証では、回路を複数の法について個別に検証する。剰余数表現で知られているように、もとの関数の剰余の組で、もとの関数を完全に表せるので、検証においても各剰余毎の検証で良い。研究ではまず剰余BDDを組み合わせ回路の検証に適用し、ある程度の効果を確認した。また、乗算器など算術演算回路を含む順序回路の検証への適用についても研究を行なった。第三に、プロセッサの検証などで重要な、回路の構造に基づく縮約手法の研究を行ない、論理回路をグラフと見て、構造が等しい部分を縮約するという手法の研究を行なった。さらに、時相論理に基づく仕様記述法について研究を行ない、仕様記述から仕様記述に関係のない回路部分を縮約する手法の研究を行なった。