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