|
1.SATベースの形式的検証やタイミング解析の高速化のためのBDDを用いたCNF式生成手法の開発を行った。
論理式の充足可能性判定(Satisfiability ; SAT)を用いた論理回路の形式的検証やタイミング解析の高速化を目指し、論理回路からSATソルバの実行時間が短くなるような和積標準形(Conjunctive Normal Form ; CNF)論理式を生成する、CNF式生成処理フレームワークを提案した。一般に論理回路のCNF式表現は一意でない上、充足可能性判定に要する時間はSATソルバに与えるCNF式により変化する。そのため、CNF式の生成処理は、SATベースの形式的検証の高速化をはかる上で重要な問題である。提案フレームワークは、回路分割と、部分回路の二分決定グラフ(Binary Decision Diagram ; BDD)生成、BDDからCNF式への変換から構成される。提案フレームワークは、回路を分割し、分割で得られた部分回路のBDDを構築し、BDDからCNF式を生成する。SATソルバの実行時間の短縮に効果のある、回路分割、部分回路のBDD生成、BDDからCNF式への変換の、各アルゴリズムの研究を進めることにより、論理回路の形式的検証やタイミング解析の高速化を目指す。提案フレームワークに基づく、中間変数の間隔を考慮した回路分割、BDD生成、BDDからCNF式への変換アルゴリズムを開発した。提案するCNF式生成手法と広く用いられているCNF式生成手法を実装し、SATソルバの実行時間について比較を行ったところ、提案手法により実行時間が短縮されることが確認された。
|
