プルーフチェッカーを用いた超並列演算器の設計検証

点击翻译按钮获取中文摘要

「ロジック」の問題に関して,演算回路を数学的定義に基づいて設計し,設計検証と動作の正しさをプルーフチェッカー(Proof Checker)を用いて証明する方策について検討した.回路を定義していくための数学的概念は,回路の構造として,回路内の全信号点を表す状態空間,入出力信号間の写像で定義される演算子,演算に必要な入力信号点を表す演算子から信号点への写像,および演算結果を表す演算子から出力信号点への写像,といった4つの空間と写像の対として定義する,多ソート代数構造を用いた.これは,従来のシミュレーション手法などで用いている,狭い条件下での演算子,信号線,遅延情報の組とは異なり,信号点の状態空間を0/1の値だけをとり得る2値空間だけでなく,ハイインピーダンス状態や連続空間など,様々な空間で回路を定義できることを示す.この構造を基に,入力信号により出力信号が一意に決定できる演算子を一つだけ持つような演算回路を定義した.この結果,演算子が当該回路の入出力信号点の間を写像する関数として正当か,結果が一意に定まる関数が存在するか,入力信号点の状態が変化した場合,演算結果が安定となるか,などの重要な性質が数学的に証明可能であることを示した.次に,演算回路の合成について定義する.合成後の回路は,上述の構造における各空間・写像の和をとったものであり,この合成回路に関しても,結果が一意に定まるか,演算結果が安定となるか,などの性質が証明可能となった.本研究の目標は,現在有力視されている代数計算モデルのうち,多ソート代数モデルを取り上げ,正当性の証明をプルーフチェッカーを用いることにある.更に,検証済みの計算モデルをVHDL(ハードウェア記述言語)などへ自動変換し,FPGA(Field Programmable Gate Array)などの試作用デバイスを用いて並列演算器の実装の行い,動作の検証を行う必要がある.それにより,設計検証方法による動作原理の違いを明確にし,信頼性の高い演算器実装に関する数理的手法を確立する.本年度は,次の2つの展開研究を並行して進めた.(1)計算モデルを基にした回路から,ゲートアレイ配置配線ソフトウェアによりターゲットデバイス用の配置配線情報を生成した。各プロセッサ要素には,計算モデル上で動作の正当性を検証済みの高速加算・減算器,並列配列型乗算器などを搭載している.これにより,動作時における動的再構成などが容易なマルチコンテクスト・ハードウェアの構成が可能となった(2)「多ソート代数モデル」による並列演算器の計算モデルを昨年度作成したが,この拡張として,高速演算性を実現するためのキャリー先見回路やキャリーモニタ回路を有した超高速加算器などの数学モデルを構築した。定義は数学的帰納法を用い,自然数Nのオーダーで計算モデルを作成した。その後、プルーフチェッカーで証明可能とした.