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

ハードウェアの機能レベル設計に対する形式的検証手法に関する研究

硬件功能级设计的形式化验证方法研究

基本信息

批准号：
10780189
负责人：
濱口清治
金额：
$ 0.9万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1998
资助国家：
日本
起止时间：
1998 至 1999
项目状态：
已结题

项目摘要

本研究は、論理レベルよりも高位の記述、特に機能レベルと呼ばれる設計記述に対する形式的検証の自動化を目標としている。仕様記述には第1階述語論理の部分クラスを用いる。これにより、算数演算器などを論理レベルに展開することなく、高い抽象度のままで直接扱うことができる。仮定している部分クラスでは、等価性判定が容易であるため、自動検証が従来の論理レベルよりも抽象度の高いレベルで可能になる。本器研究では、まず、第一階述語論理の部分クラスを遷移関数の記述に用いることができるよう拡張した拡張順序機構に対する検証について検討した。具体的には、第1階述語論理の部分クラスに時相演算子を加えた論理体系を示して、これを性質の記述に用いた場合の検証アルゴリズムを示した。また、機能レベル記述とレジスタ転送レベルの記述を比較するためには、たとえ出力のタイミングが異なっていても、等価であるとみなさなければならない場合があるが、これについて、2つの拡張順序機械に対し、出力信号値が変化した直後の値同士を比較するアルゴリズムを考察した。以上の結果をもとに、まず、基礎となる第一階述語論理の部分クラスに対する恒真性判定アルゴリズムの実装を行った。次に、これを用いて、上記の2つのアルゴリズムの実装し、いくつかの例題について実験を行った。今回作成したプロトタイプは、検証に非常に多くのの時間と記憶領域を必要とする。これに対して、第一階述語論理の部分クラスに対する恒真性判定アルゴリズムについて、命題論理式に対する高速充足可能性判定システムを利用する手法を実装し、実験を開始しているほか、検証アルゴリズムそのものについても、いくつかの効率改善手法を検討しており、ひきつづき詳細化および実験を行っていく予定である。

This study aims to automate the design of high-level descriptions, special functions, and related forms of identification. Description of the first order predicate logic part of the use of This is the first time that an algorithm has been developed. It is easy to determine the equivalence of some parts, and it is possible to automatically verify the logical equivalence of some parts. This paper studies the description of the transfer relationship between the first order predicate logic and the second order predicate logic. The concrete description of the first order predicate logic is shown in the case where the phase operator is added to the logic system The description of the output signal is different from the description of the output signal. The description of the output signal is different from the description of the output signal. The description of the output signal is different from that of the output signal. The results of the above are as follows: first order predicate logic, second order predicate logic, third order predicate logic, third order predicate logic, fourth order predicate logic, fourth order predicate logic, fourth The second, the third, the third, the fourth, the This time around, we're going to make sure that there's a lot of time and memory that's necessary. For this reason, the first order statement logic is used to determine the constant truth, and the propositional logic is used to determine the high speed sufficiency. The method of implementation, implementation, and verification of the constant truth is used to determine the middle and middle of the efficiency.