2012 Fiscal Year Research-status Report
グリッド環境の定理証明器とモデル検査器をハードウェアコンパイラ融合した形式検証系
Project/Area Number |
23500174
|
Research Institution | Shinshu University |
Principal Investigator |
和崎 克己 信州大学, 工学部, 教授 (70271492)
|
Keywords | 探索・論理・推論アルゴリズム / 定理証明器 / コンパイラ / 関数型言語系 |
Research Abstract |
定理証明器(プルーフチェッカ, Proof Checker)と,様々なターゲット実装コードを出力可能なハードウェアコンパイラを融合し,上流から下流工程まで一貫した高機能な形式検証系を構築し,非同期並列回路システムの検証能力の飛躍的向上を図る. 対象回路の構成情報は,関数型言語系の上で記述し,この言語系からのコンパイラ出力として,ターゲット実装コードと,プルーフチェッカへの証明式の列を同時に得る. 検証対象は,パイプラインあるいはトーラス接続された超並列演算器(PE)である.この設計検証のために,プルーフチェッカを用いてプロパティ検証を実行する.上位の超並列接続のための制御器のモデルによって多数の PE をネットワーク・オートマタによって論理接続する.対象回路の構成情報は,簡易な回路記述に文法を縮約した,一種の関数型プログラミング言語系の上で記述し,この言語系からのコンパイラ出力として,プルーフチェッカが処理できる形式の数式定義,定理証明列を得るものとする. 上記の目的のため,関数型言語系の上にハードウェアコンパイラを開発した.対象回路の構成情報は,簡易な回路記述に文法を縮約した,一種の関数型プログラミング言語系の上で記述し,この言語系からのコンパイラ出力として,モデル検査器ならびにプルーフチェッカが処理できる形式の数式定義,定理証明列が自動的に得られるようにした.対象関数型言語系として,Objective Caml を使用する.並列構成時に必要な高位設計記述のため,COINSコンパイラ基盤を用いて,水平・垂直分散モジュールのインターフェース定義から中間系への自動変換を行う援用プログラムも並行して作成した.
|
Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の順序としては,まず,(1)関数型言語系の上のハードウェアコンパイラを機能拡張し,(2)実際の回路規模を対象とした各種検証系向けコード生成器の性能評価を実施し,次に,(3)定理証明器ならびにモデル検査器 を,グリッドコンピューティング環境上へ実装する,という計画となっている.引き続いて,システム統合のため,(4)状態空間の分割・合成を行うためのアルゴリズム開発と並列化ライブラリを利用したプログラム開発を行うこととなっている. 上記項目(1)の機能拡張については平成23年度において実施した.具体的には,Objective Caml 関数型言語系を台言語として,その上のSyntax sugar として再帰的データ構造を用いたsub-circuit定義向けの回路記述モジュールを構築し,対象並列回路をスケーラブルな形で記述可能にすることに成功した. 上記項目(2)の実施については平成24年度において順調に推移した.回路記述モジュールが生成する回路情報の内部表現(中間系)に基づき,Verilog-HDL や VHDL といった下位ハードウェア記述言語向けのコード生成器を開発した. 上記項目(3)の実施については,これは平成24年度においては検証環境の構築を行うこととなっており,定理証明器(プルーフチェッカ)とモデル検査器に対して,並列コア搭載高性能プロセッサ上での稼働性能評価ならびにネットワーク接続されたPCクラスタ機(現有設備)を用いた性能評価を継続的に行った. 上記項目(4)については,COINSコンパイラ基盤を用いて現在の所,設計・開発を継続中である.
|
Strategy for Future Research Activity |
次年度は,本年度に構築した[A]並列化検証システムの性能評価を行う.対象回路の構成情報は,簡易な回路記述に文法を縮約した,一種の関数型プログラミング言語系の上で記述する.特に, モデル検査器とプルーフチェッカを,グリッドコンピューティング環境上へ実装する.ミドルウェアとして Globus-2 ,並列化ライブラリとして MPICH-G2 を使用する.システム統合のため,証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラム開発を行う 引き続いて[B]クラスタ計算機上の並列化検証システムの速度性能向上のため,CUDA-GPU 並列アクセラレータを導入し,検証済み演算器のシミュレーション・形式検証統合システムを完成する.この時,各演算用のクラスライブラリを作成し,回路情報と計算モデルとのマッチングを行うための方策を検討する. 最後に,これまでに得られた結果を基にして,関数型言語系の上のハードウェアコンパイラと,グリッド環境上の高性能並列検証システムとを結合利用し,実際の回路規模のLSI設計データ等を対象とし,FPGA/CPLD統合設計開発ツールを導入し,検証系全体のユーザビリティ評価を実施する.
|
Expenditure Plans for the Next FY Research Funding |
該当なし
|
Research Products
(10 results)