Multi-clock path analysis using propositional satisfiability

We present a satisfiability based multi-clock path analysis method. The method uses propositional satisfiability (SAT) in the detection of multi-clock paths. We show a method to reduce the multi-clock path detection problems to SAT problems. We also show heuristics on the conversion from multi-level circuits into CNF formulae. We have applied our method to ISCAS89 benchmarks and other sample circuits. Experimental results show the improvement on the manipulatable size of circuits by using SAT.

• Type: Conference
• Year: 2000
• Where: ASPDAC
• Authors: Kazuhiro Nakamura, Shinji Maruoka, Shinji Kimura, Katsumasa Watanabe
• Keywords: ASPDAC 2000, Hardware, Multi-clock Path, Path Analysis Method, Path Detection Problems