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

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

基本信息

批准号：
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 Sorba中的处理时间取决于给定的CNF类型，因此将逻辑电路转换为CNF类型的过程是对SAT的正式验证和时间分析基础。在此转换过程中，开发了一种算法，其中将逻辑电路分为风扇外点并转换为每个部分电路的CNF类型。实施了所提出的算法并评估了SAT Sorba的执行时间，并与常规转换相比，确认了SAT求解器的执行时间的缩短。这项研究的结果在国内研究小组宣布。此外，我们开发了一种1速反检测方法，用于正式验证订单电路并加快计时分析。为了提高正式验证和定时分析的准确性，对可以从初始状态达到的状态进行准确分析很重要。 1-HOT计数器通常用于高速阶回路的设计中，但是可以获得的数字是有限的，因此无法达到许多情况。检测1-HOT计数器并分析可以更准确地达到的状态，从而导致对顺序电路的形式验证以及定时分析的准确性，包括1-HOT计数器。除了制定1-HOT反检测问题外，还开发了1-HOT反检测算法。这项研究的结果在国内研究小组宣布。