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

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

基本信息

批准号：
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カウンタ検出アルゴリズムの開発を行った。本研究の成果は国内研究会で発表した。

我们已经开发了一种电路划分方法，用于生成结合性正常形式（CNF）逻辑表达式，以创建满足性（SAT）的正式验证和时机分析。逻辑电路的CNF表达表示并非唯一，并且SAT求解器中的处理时间取决于给定的CNF表达式，因此将逻辑电路转换为CNF表达式的过程对于加快SAT碱基和时间分析的正式验证而言很重要。在此转换过程中，开发了一种算法，该算法将逻辑电路分配在风扇外点，并将其转换为每个部分电路的CNF方程。当我们实施建议的算法并评估了SAT求解器的执行时间时，我们能够确认与常规转换器相比，SAT求解器的执行时间缩短了。这项研究的结果是在一个国内研究小组中提出的。此外，我们开发了一种1速反检测方法，用于正式验证顺序电路并加快定时分析。对初始状态和可到达状态的准确分析对于提高正式验证和定时分析的准确性很重要。 1速计数器通常用于高速顺序电路的设计，但是由于可能的值有限，许多状态无法实现。检测1-HOT计数器并更准确地分析可达状态，从而提高了包括1-HOT计数器在内的顺序电路的形式验证和定时分析。除了制定1速逆检测问题外，我们还开发了一种1速逆检测算法。这项研究的结果是在一个国内研究小组中提出的。