充足可能性判定手法に基づいたマルチクロックパス解析  [in Japanese] Multi-Clock Path Analysis Based on Propositional Satisfiability  [in Japanese]

通常,順序回路のタイミング検証は,レジスタ間の信号伝搬が全て1クロックであるという仮定のもとで行われるが,2クロックで伝搬しても良い経路(マルチクロックパス)の存在が知られており,そのような経路を特定してタイミング検証を行うことが重要である.これまでに,記号実行を用いたマルチクロックパスの解析手法が提案されているが,大規模回路への適用が困難であった.本論文では,論理式の充足可能性を判定するSATアルゴリズムの応用によりマルチクロックパス解析を行う手法を提案する.

We present a satisfiability based multi-clock path analysis method. Multi-clock paths are paths between registers where the propagation of signals can use more than 1 clock cycle. Multi-clock path analysis is important in deciding proper clock frequency and for logic optimization. At present, we only have methods based on state traversal which can be applied to medium sized circuits. In the paper we propose a new multi-clock path analysis method based on propositional satisfiability (SAT). The method reduces path analysis problems to SAT problems by converting the time-expanded multilevel circuit to CNF formula, and improves the size of applicable circuits. We introduce heuristics on converting multi-level circuits to CNF formulae to reduce the size of the formula and the time consumed by SAT procedure. We have applied our method to ISCAS89 benchmarks and other sample circuits. Experimental results show the improvement on the applicable size of circuits by our method.