2013 Fiscal Year Annual Research Report
グリッド環境の定理証明器とモデル検査器をハードウェアコンパイラ融合した形式検証系
| Project/Area Number |
23500174
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 信州大学, 工学部, 教授 (70271492)
|
|---|
| Keywords | 探索・論理・推論アルゴリズム / 定理証明器 / コンパイラ / 関数型言語系 |
|---|
| Research Abstract |
定理証明器(プルーフチェッカ, Proof Checker)と，様々なターゲット実装コードを出力可能なハードウェアコンパイラを融合し，上流から下流工程まで一貫した高機能な形式検証系を構築し，非同期並列回路システムの検証能力の飛躍的向上を図る． 対象回路の構成情報は，関数型言語系の上で記述し，この言語系からのコンパイラ出力として，ターゲット実装コードと，プルーフチェッカへの証明式の列を同時に得る．
検証対象は，パイプラインあるいはトーラス接続された超並列演算器(PE)である．この設計検証のために，プルーフチェッカを用いてプロパティ検証を実行する．上位の超並列接続のための制御器のモデルによって多数の PE をネットワーク・オートマタによって論理接続する．対象回路の構成情報は，簡易な回路記述に文法を縮約した，一種の関数型プログラミング言語系の上で記述し，この言語系からのコンパイラ出力として，プルーフチェッカが処理できる形式の数式定義，定理証明列を得るものとする．
平成24年度に作成した関数型言語上のハードウェアコンパイラについて，並列化検証システムの性能評価を行った．対象回路の構成情報は，簡易な回路記述に文法を縮約した，一種の関数型プログラミング言語系の上で記述した．特に， モデル検査器とプルーフチェッカを，グリッドコンピューティング環境上へ実装した．システム統合のため,証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラム開発を行った．続いて，クラスタ計算機上の並列化検証システムの速度性能向上のため，CUDA-GPU 並列アクセラレータを導入し，検証済み演算器のシミュレーション・形式検証統合システムを完成した．この時，各演算用のクラスライブラリを作成し，回路情報と計算モデルとのマッチングを行うための方策を検討した．
|
