論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法

摘要

本稿では、SATを用いた論理回路の形式的検証の高速化を目指し、論理回路からSAT-solverの実行時間が短かくなるような和積標準形CNF論理式を生成する、CNF式生成処理フレームワークを提案する。 提案するフレームワークは、回路分割と、部分回路のBDD生成、BDDからCNF式への変換から構成される。 また本稿では、提案フレームワークに基づく、中間変数の間隔を考慮した回路分割、BDD生成、BDDからCNF式への変換アルゴリズムを示す。 提案するCNF式生成手法と広く用いられているCNF式生成手法を実装し、SAT-solverの実行時間について比較を行ったところ、提案手法により実行時間が短縮されることが確認された。