複数の制御部をもつ同期式順序回路の機能検証に関する研究

Research Project

Project/Area Number	07680356
Research Category	Grant-in-Aid for General Scientific Research (C)
Allocation Type	Single-year Grants
Research Field	計算機科学
Research Institution	Osaka University
Principal Investigator	谷口健一大阪大学, 基礎工学部, 教授 (00029513)
Co-Investigator(Kenkyū-buntansha)	岡野浩三大阪大学, 基礎工学部, 助手 (70252632) 北道淳司大阪大学, 基礎工学部, 助手 (20234271) 松浦敏雄大阪市立大学, 生活科学部, 教授 (40127296) 東野輝夫大阪大学, 基礎工学部, 助教授 (80173144)
Project Period (FY)	1995
Project Status	Completed (Fiscal Year 1995)
Budget Amount *help	¥2,000,000 (Direct Cost: ¥2,000,000) Fiscal Year 1995: ¥2,000,000 (Direct Cost: ¥2,000,000)
Keywords	同期式順序回路 / 拡張有限状態機械 / レジスタ転送レベル / 設計検証 / 形式的検証 / 代数的手法 / プレスブルガ-算術 / パイプラインCPU
Research Abstract	(1)複数制御部を持つ回路が要求仕様(CPUなどの回路の機能記述)を満たすという意味で正しい実現であるという形式的な定義を行い,単一制御部を持つとして書かれた要求仕様から,複数制御部を持つレジスタ転送レベルの回路を段階的に設計する方法,および設計の正しさの証明法を検討した(1.情報処全大1996-03),その手順は次のようなものである:(i)まず,単一制御部を持つレジスタ転送レベルの回路を設計し、それが要求仕様を満たすことを証明する,(ii)制御部を複数個の拡張有限状態機械(EFSM)に分割する.分割の正しさの証明では,分割前のEFSMと分割後の各EFSMを,整数上の論理式の真偽判定ルーチンにより遷移の実行条件を調べつつトレース実行し,同じ演算・データ転送が行われることを調べる. (2)考案した設計法・証明法の有用性を調べるため,証明をなるべく自動で行うための証明支援系のプロトタイプを作成し,市販のパイプライン方式CPUのサブセットを例題に,設計・証明実験を行った.パイプライン方式CPUは,通常,命令パイプラインの各ステージの動作を制御する複数個の制御部を持つ.上記(1)の手順(i)の適用例として,パイプライン方式CPUを,まず単一制御部で実現する設計法・証明法を検討し(2.情報処理学会研究報告1996-02),試作した証明支援系でその正しさの証明が数時間程度で自動で行えることを確かめた.制御部の分割の正しさの証明等まで含めた設計・証明実験の結果について,学会研究会等で発表する予定である. (3)一方,証明支援系で用いる整数上の論理式の真偽判定ルーチンを,論理式の構造的な特徴を巧く利用して高速化し(3.信学技報1995-07),より実用的な証明支援系にした.