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