| 研究概要 |
(1)複数制御部を持つ回路が要求仕様(CPUなどの回路の機能記述)を満たすという意味で正しい実現であるという形式的な定義を行い,単一制御部を持つとして書かれた要求仕様から,複数制御部を持つレジスタ転送レベルの回路を段階的に設計する方法,および設計の正しさの証明法を検討した(1.情報処全大1996-03),その手順は次のようなものである:(i)まず,単一制御部を持つレジスタ転送レベルの回路を設計し、それが要求仕様を満たすことを証明する,(ii)制御部を複数個の拡張有限状態機械(EFSM)に分割する.分割の正しさの証明では,分割前のEFSMと分割後の各EFSMを,整数上の論理式の真偽判定ルーチンにより遷移の実行条件を調べつつトレース実行し,同じ演算・データ転送が行われることを調べる.
(2)考案した設計法・証明法の有用性を調べるため,証明をなるべく自動で行うための証明支援系のプロトタイプを作成し,市販のパイプライン方式CPUのサブセットを例題に,設計・証明実験を行った.パイプライン方式CPUは,通常,命令パイプラインの各ステージの動作を制御する複数個の制御部を持つ.上記(1)の手順(i)の適用例として,パイプライン方式CPUを,まず単一制御部で実現する設計法・証明法を検討し(2.情報処理学会研究報告1996-02),試作した証明支援系でその正しさの証明が数時間程度で自動で行えることを確かめた.制御部の分割の正しさの証明等まで含めた設計・証明実験の結果について,学会研究会等で発表する予定である.
(3)一方,証明支援系で用いる整数上の論理式の真偽判定ルーチンを,論理式の構造的な特徴を巧く利用して高速化し(3.信学技報1995-07),より実用的な証明支援系にした.
|
