Multi-cycle path detection based on propositional satisfiability with CNF simplification using adaptive variable insertion

Multi-cycle paths are paths between registers where 2 or more clock cycles are allowed to propagate signals, and the detection of multi-cycle paths is important in deciding proper clock period, timing verification and logic o ptimization. This paper presents a satisfiability-based multi-cycle paths d etection method, where the detection problems are reduced to CNF formulae a nd the satisfiability is checked using SAT provers. We also show heuristics on conversion from multi-level circuits into CNF formulae. We have applied our method of ISCAS'89 benchmarks and other sample circuits. Experimental results show the remarkable improvements on the size of manipulatable circu its.