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

論理回路の縮約モデルの自動抽出とそれを用いた大規模論理回路の設計検証に関する研究

逻辑电路简化模型自动提取及大规模逻辑电路设计验证研究

基本信息

批准号：
07780268
负责人：
木村晋二
金额：
$ 0.58万
依托单位：
Nara Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07780268/
关键词：
形式的検証二分決定グラフ BDD 論理設計検証剰余BDD

项目摘要

本研究では、論理回路の縮約モデルの抽出と、それを用いた大規模論理回路の検証に関する研究を行った。まず、縮約モデルを用いた検証手法に関する調査研究を行なった。つぎに現在多くの論理設計検証手法で用いられている二分決定グラフ(Binary Decision Diagram、BDD)について研究を行なった。特に回路の内部の適当な論理ゲートの出力を変数として扱ってBDDを小さくするとともに、相異なる内部変数を持つ二つの回路の等価性判定を行なう手法の研究を行なった。等価性判定では、一方の回路の内部変数を他方の回路の内部変数へ多項式時間で変換する手法を新たに開発して用いた。第二に、乗算など算術演算回路で二分決定グラフの節点爆発を抑制する手法を提案した。これは数の剰余数表現に基づく手法で、算術演算回路の入力が二進数に対応づけられているという性質を用い、二分決定グラフの節点数を入力変数の数の多項式で限定する。限定された結果のBDDを剰余BDD(Residue BDD)と呼ぶ。検証では、回路を複数の法について個別に検証する。剰余数表現で知られているように、もとの関数の剰余の組で、もとの関数を完全に表せるので、検証においても各剰余毎の検証で良い。研究ではまず剰余BDDを組み合わせ回路の検証に適用し、ある程度の効果を確認した。また、乗算器など算術演算回路を含む順序回路の検証への適用についても研究を行なった。第三に、プロセッサの検証などで重要な、回路の構造に基づく縮約手法の研究を行ない、論理回路をグラフと見て、構造が等しい部分を縮約するという手法の研究を行なった。さらに、時相論理に基づく仕様記述法について研究を行ない、仕様記述から仕様記述に関係のない回路部分を縮約する手法の研究を行なった。

This paper is a study on the extraction and application of reduced logic circuits in large-scale logic circuits. The investigation and study on the application of the new method of identification and reduction shall be conducted. The method of logic design verification is used in Binary Decision Diagram (BDD). A study on the method of determining the equivalence of a special loop by determining the internal variation of the appropriate logic component of the loop. A new method for determining equivalence is proposed, which is to change the internal number of one loop to the internal number of the other loop. Second, the arithmetic loop is divided into two parts to determine the node explosion suppression method. The number of nodes in a binary arithmetic loop is determined by the number of inputs in a polynomial. BDD(Residue BDD) The method of identification is multiple, and the method of identification is multiple. The remainder is represented by the number of pairs. The results of this study confirm the suitability of the BDD system for testing and evaluation. The application of the algorithm, the algorithm loop, the sequence loop and the verification loop is studied. The third is to study the basic reduction method of circuit structure, and to study the reduction method of logic circuit structure. In addition, the study of time and phase logic, basic description method, research method and reduction method