論理関数処理による記号シミュレーションと無解釈評価に基づくプロセッサの形式的検証

基于符号模拟和使用逻辑函数处理的非解释评估的处理器形式验证

• 批准号: 07780258
• 负责人: 石浦 菜岐佐
• 金额: $ 0.58万
• 依托单位: Osaka University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07780258/
• 关键词: 設計検証; 論理関数; 二分決定グラフ; モデルチェッキング; マイクロプロセッサ

本研究では形式的検証法をプロセッサに適用することを試みた.できる限り大規模なハードウェアに形式的検証法を適用するための計算手法の開発を目標に研究を進め,「記号シミュレーション」と「無解釈評価」を用いた方法に基づく処理系の試作とその評価を行なった.(1)アルゴリズムの検討現在までに得られているアイデアを具体化し,計算機上での処理に適した計算手順をまとめた.検証したいプロセッサの動作を,リファレンスプロセッサとよぶ単純なハードウェアで同じ命令セットを実行するプロセッサと比較する.この際に,複雑な算術演算は,同じ計算が行なわれたことだけを完全に検証することにより,計算量を大幅に削減した.(2)処理系の実現2つのプロセッサの動作の比較は,順序機械の記号モデル検査法のプログラムであるSMV(CMUで開発されたもの)を用いて行なった.「パイプラインALU」と呼ばれる小規模例題による実験と,DLXプロセッサに対して適用を行ない,3,000ゲートレベルのプロセッサまでなら30時間程度で検証が行なえる目処がついた.しかし,これ以上の規模のプロセッサに適用するには,さらに工夫が必要であることが判明した.(3)論理関数処理の新しいアルゴリズムの考案検証の時間とほとんどは,論理関数処理に費やされる.これまで,二分決定グラスを用いた手法が用いられてきたが,この方法ではメモリ要求が爆発的に増大する例が知られていた.本研究では,このような問題に対して,二分決定グラフのグラフ構造を非明治的に論理関数表現し,これを再び二分決定グラフで表すというデータ構造と,これに対するアルゴリズムを開発し,その評価を行なった.

In this study, the method in the form of medicine is used in this study. In the form of large-scale computer simulation, the method of computer simulation has been used to study the progress of the study, which is not understandable. (1) it is possible to use the basic theory system to improve the performance of the system. (1) the system of computer science is responsible for the implementation of the computer system. (1) the system of computer science is responsible for the implementation of the system. (1) the system of computer science has been able to make it more specific. The computer is responsible for the operation of the computer. I don't know what to do. I don't know. I don't know. I don't know what to do. In the same way as the calculation of the computer, the calculation, the calculation. The sequence of mechanical records shows that the SMV (CMU operating system) is used for monitoring the operation of the computer. The model of the system is called for the model of the failure of the system. The model of the DLX is used for the monitoring of the operating system, and the operating system is used for the purpose of monitoring the operating system. 3000 percent of the time is required for the monitoring of the operating system, and the monitoring of the operating system for 30 days. It is necessary to make sure that it is necessary to determine the accuracy of the examination. (3) to make sure that the examination plan is in good time, and that it is necessary to make sure that it is necessary to make a correct decision. In two parts, it is decided that the method should be used in the first place, and that the method would require a lot of information. In this study, we decided that we should make a list of non-Meiji figures, and then decide that the table should be completed, and that we should start the operation.

项目成果

Hitoshi Yamauchi: "Implicit Representation and Manipulation of Binary Decision Diagrams" IEICE Trans.Fundamentals. E-79A(to appear). (1996)

Hitoshi Yamauchi：“二元决策图的隐式表示和操作”IEICE Trans.Fundamentals。