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

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

基本信息

批准号：
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-hot 计数器检测方法来加速时序电路的形式验证和时序分析。准确分析从初始状态可到达的状态对于提高形式验证和时序分析的准确性非常重要。 1-hot计数器常用于高速时序电路的设计中，但由于其可能的值有限，很多状态是无法到达的。更准确地检测 1-hot 计数器并分析可达状态将提高包含 1-hot 计数器的时序电路的形式验证和时序分析的准确性。我们制定了 1-hot 计数器检测问题并开发了 1-hot 计数器检测算法。该研究成果在国内的一次研究会议上进行了展示。