2009 Fiscal Year Annual Research Report
関数型言語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法
| Project/Area Number |
20500130
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 Shinshu University, 工学部, 教授 (70271492)
|
|---|
| Keywords | 形式検証 / 関数型言語系 / グリッド計算機 / プルーフチェッカ / 設計検証系 / 並列演算器 |
|---|
| Research Abstract |
平成21年度においては、ハードウェアコンパイラの作成と並列化プルーフチェッカの性能評価を行った。対象回路の構成情報は、簡易な回路記述に文法を縮約した、一種の関数型プログラミング言語系の上で記述し、この言語系からのコンパイラ出力として、プルーフチェッカが処理できる形式の数式定義、定理証明列が自動的に得られるようにした。性能評価のために、ゲートアレイ配置配線ソフトウェアを使用し、検証済み演算器のシミュレーション・形式検証統合システムを拡充した。以下に各ステップの詳細について述べる。
(1)関数型言語系上のハードウェアコンパイラ開発
対象回路の構成情報は、簡易なり回路記述に文法を縮約した、一種の関数型プログラミング言語系の上で記述し、この言語系からのコンパイラ出力として、プルーフチェッカが処理できる形式の数式定義、定理証明列が自動的に得られるようにした。Verilog-HDLやVHDLなどのハードウェア記述言語から、関数型言語系への自動変換を行う援用プログラムも並行して作成した。
(2)並列化プルーフチェッカの性能評価
検証対象は、パイプラインあるいはトーラス接続された並列演算器(PE)とした。計算を多ソート代数でモデル化し、超並列接続のための制御器のモデルによって多数のPEをネットワーク・オートマタによって論理接続することとした。
(3)形式検証系に関する海外共同研究者(Canada, France)との合同調査研究の継続
実施体制としては、・申請者:並列化システム構築とコンパイラ開発、・Canada研究者:ネットワーク・オートマタによる問題分割の理論検討、・France研究者:検証対象(超並列演算器)の仕様作成と関数型言語系の保守、という構成をとった。
|
