2011 Fiscal Year Research-status Report
グリッド環境の定理証明器とモデル検査器をハードウェアコンパイラ融合した形式検証系
| Project/Area Number |
23500174
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 信州大学, 工学部, 教授 (70271492)
|
|---|
| Project Period (FY) |
2011-04-28 – 2014-03-31
|
| Keywords | 探索・論理・推論アルゴリズム / 定理証明器 / コンパイラ / 関数型言語系 |
|---|
| Research Abstract |
定理証明器(プルーフチェッカ, Proof Checker)と，様々なターゲット実装コードを出力可能なハードウェアコンパイラを融合し，上流から下流工程まで一貫した高機能な形式検証系を構築し，非同期並列回路システムの検証能力の飛躍的向上を図る． 対象回路の構成情報は，関数型言語系の上で記述し，この言語系からのコンパイラ出力として，ターゲット実装コードと，プルーフチェッカへの証明式の列を同時に得る． 検証対象は，パイプラインあるいはトーラス接続された超並列演算器(PE)である．この設計検証のために，プルーフチェッカを用いてプロパティ検証を実行する．上位の超並列接続のための制御器のモデルによって多数の PE をネットワーク・オートマタによって論理接続する．対象回路の構成情報は，簡易な回路記述に文法を縮約した，一種の関数型プログラミング言語系の上で記述し，この言語系からのコンパイラ出力として，プルーフチェッカが処理できる形式の数式定義，定理証明列を得るものとする． 上記の目的のため，関数型言語系の上にハードウェアコンパイラを開発した．対象回路の構成情報は，簡易な回路記述に文法を縮約した，一種の関数型プログラミング言語系の上で記述し，この言語系からのコンパイラ出力として，モデル検査器ならびにプルーフチェッカが処理できる形式の数式定義，定理証明列が自動的に得られるようにした．対象関数型言語系として，Objective Caml を使用する．Verilog-HDL や VHDL などのハードウェア記述言語から，関数型言語系への自動変換を行う援用プログラムも並行して作成した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の順序としては，まず，（１）関数型言語系の上のハードウェアコンパイラを機能拡張し，（２）実際の回路規模を対象とした各種検証系向けコード生成器の性能評価を実施し，次に，（３）定理証明器ならびにモデル検査器 を，グリッドコンピューティング環境上へ実装する，という計画となっている．引き続いて，システム統合のため，（４）状態空間の分割・合成を行うためのアルゴリズム開発と並列化ライブラリを利用したプログラム開発を行うこととなっている． 上記項目（１）の機能拡張については順調に推移した．具体的には，Objective Caml 関数型言語系を台言語として，その上のSyntax sugar として再帰的データ構造を用いたsub-circuit定義向けの回路記述モジュールを構築し，対象並列回路をスケーラブルな形で記述可能にすることに成功している． 上記項目（２）についても順調に推移している．回路記述モジュールが生成する回路情報の内部表現（中間系）に基づき，Verilog-HDL や VHDL といった下位ハードウェア記述言語向けのコード生成器を開発した．また拡張LOTOS向けのコード生成器も作成した． 上記項目（３）については，これは平成２３年度においては研究準備を行うこととなっており，定理証明器（プルーフチェッカ）とモデル検査器に対して，並列コア搭載高性能プロセッサ上での稼働性能評価ならびにネットワーク接続されたPCクラスタ機（現有設備）を用いた性能評価を行った． 上記項目（４）については，次年度以降の設計・開発を行うこととなっている．
|
| Strategy for Future Research Activity |
次年度以降は，先ず[A]並列化検証システムの性能評価を行う．対象回路の構成情報は，簡易な回路記述に文法を縮約した，一種の関数型プログラミング言語系の上で記述する．特に， モデル検査器とプルーフチェッカを，グリッドコンピューティング環境上へ実装する．ミドルウェアとして Globus-2 ，並列化ライブラリとして MPICH-G2 を使用する．高速なノード間接続のために，光高速ネットワークバスを導入し，現有設備のスレーブノード × 30 台を計算クラスタとして構成する．システム統合のため,証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラム開発を行う 引き続いて[B]クラスタ計算機上の並列化検証システムの速度性能向上のため，CUDA-GPU 並列アクセラレータを導入し，検証済み演算器のシミュレーション・形式検証統合システムを 完成する．この時，各演算用のクラスライブラリを作成し，回路情報と計算モデルとのマッチングを行うための方策を検討する．
|
| Expenditure Plans for the Next FY Research Funding |
初年度申請時の研究計画調書記載の「研究経費」使用内訳に対して，大きな変更はない．具体的には，設備備品費（光高速ネットワークバス装置，CUDA-GPU 並列アクセラレータ，等）800千円，消耗品費（計算ノード増設ハードディスク，ギガビットHUB，ケーブル配線部材，自動並列化 C++コンパイラ，等）200千円，旅費（国内・国外論文発表，研究打ち合わせ等）300千円，謝金その他 100千円，総額1,400千円の研究費使用を計画している．
|
