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

順序回路のタイミング解析の正確さ向上に関する研究

提高时序电路时序分析精度的研究

基本信息

批准号：
18700043
负责人：
中村一博
金额：
$ 1.79万
依托单位：
Nagoya University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2006
资助国家：
日本
起止时间：
2006 至 2007
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18700043/
关键词：
VLSI設計技術順序回路 SATソルバ CNF式タイミング解析論理回路 VLSI 形式的検証 BDD

项目摘要

論理式の充足可能性判定(Satisfiability;SAT)ベースの形式的検証やタイミング解析の高速化のための、和積標準形(Conjunctive Normal Form;CNF)論理式生成における回路分割手法の開発を行った。論理回路のCNF式表現は一意でない上、SATソルバでの処理時間は、与えられるCNF式により変化するため、論理回路をCNF式に変換する処理は、SATべースの形式的検証やタイミング解析の高速化を図る上で重要である。この変換処理において、論理回路をファンアウトポイントで分割し、部分回路毎にCNF式に変換するアルゴリズムの開発を行った。提案アルゴリズムを実装し、SATソルバの実行時間について評価を行ったところ、従来の変換手と比較して、SATソルバの実行時間の短縮が確認できた。本研究の成果は国内研究会で発表した。また、順序回路の形式的検証やタイミング解析の高速化のための、1-hotカウンタ検出手法の開発を行った。形式的検証やタイミング解析の正確さを向上させる上で、初期状態から到達可能な状態の正確な解析は重要である。1-hotカウンタは、高速な順序回路の設計においてよく用いられるが、とりうる値が限られているため、多くの状態が到達不能である。1-hotカウンタを検出し、到達可能な状態をより正確に解析することが、1-hotカウンタを含む順序回路の形式的検証やタイミング解析の正確さ向上につながる。1-hotカウンタ検出問題の定式化を行うとともに、1-hotカウンタ検出アルゴリズムの開発を行った。本研究の成果は国内研究会で発表した。

Satisfiability (SAT) of logical expressions is the form of the evaluation, analysis, and product of high-speed Normal form (CNF) of logical expression generation. The CNF expression of logic loop has the same meaning as that of SAT, and the processing time of SAT is very important. This conversion process, the logic loop is divided into two parts, the partial loop is divided into two parts, and the partial loop is divided into three parts. The proposal is to complete the installation, SAT completion time, evaluation, handover and comparison, SAT completion time shortening and confirmation. The results of this study are presented to the domestic research society. The development of a 1-hot detection method for high-speed detection of the sequence loop The correct analysis of the form is important for the initial state to arrive at the possible state. 1-hot, high speed, sequential loop design, high speed, high speed 1-hot mode detection, arrival possible mode detection, 1-hot mode detection. 1-hot The results of this study are presented to the domestic research society.