权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

多控制单元同步时序电路功能验证研究

基本信息

批准号：
07680356
负责人：
谷口健一
金额：
$ 1.28万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至无数据
项目状态：
已结题

项目摘要

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

(1)Multiple control units hold loop requests (Description of CPU loop function) Definition of the form of CPU, single control unit, multiple control unit, single control unit, single control unit,(1. Information Department, 1996-03), the sequence of operations is as follows:(i) the design of a single control unit, the design of a single control unit, The proof of the division is that the EFSM before the division and the EFSM after the division are true and false, and the logical expression on the integer is true and false. (2)The usefulness of the design method and proof method of the test case is adjusted, and the proof is automatically executed. The proof support system is automatically executed. The CPU is automatically executed. The CPU normally commands a plurality of control units to control the operation of each event. A discussion of the design method and proof method for the implementation of the above procedure (i) is given in the paper (2). Research Report of the Information Processing Society, 1996-02). The division of the control department and the verification of the results include the design, verification and verification of the results, and the establishment of the academic research meeting. (3)On the one hand, the proof support system uses the integer to determine the authenticity of the logical expression, and the structural characteristics of the logical expression are skillfully utilized to speed up (3. Information Technology Journal 1995-07).