|
論理式の充足可能性判定(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カウンタ検出アルゴリズムの開発を行った。本研究の成果は国内研究会で発表した。
|
