2008 Fiscal Year Annual Research Report
関数型言語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法
| Project/Area Number |
20500130
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 Shinshu University, 工学系研究科, 准教授 (70271492)
|
|---|
| Keywords | 形式検証 / 関数型言語系 / グリッド計算機 / プルーフチェッカ / 設計検証系 / 並列演算器 |
|---|
| Research Abstract |
プルーフチェッカ(Proof Checker)を、グリッドコンピューティング環境上へ実装し、超並列回路システムの検証能力の飛躍的向上を図る。対象回路の構成情報は、関数型言語系の上で記述し、この言語系からのコンパイラ出力として、プルーフチェッカへの証明式の列を得る。対象回路は、論理演算器の計算を多ソート代数でモデル化し、証明はプルーフチェッカを用いて検証する。論理演算子、演算子とハードウェアゲートとの関係、ゲート同士の信号線による接続等の定義・定理を基に、回路を結合・合成し,演算回路が正しく動作することを検証する。形式検証系としてMizar証明検査システムを用いる。今年度においては(1)「多ソート代数モデル」による並列演算器の計算モデルを作成した。高速演算性を実現するための加算キャリー先見回路やモニタ回路、ならびにRSD数系を利用したCarry-save generic Adderが必要だが、これらの演算素子を、自然数Nのオーダで帰納的な計算モデルとして構成し、プルーフチェッカによる数学的帰納法で証明可能とした。(2)並列性実現のため「パイプライン機構」を説明する計算モデルとして、ペトリネット表現モデルを導入した。ペトリネットによって分割・合成されたネットワーク・オートマタによりノードあたり証明問題サイズの縮小を図った。(3)プルーフチェッカを、グリッドコンピューティング環境上へ実装する準備を行った。システム統合のため,証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラムの検討を行った。
|
