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

Kazuhiro Nakamura, Shinji Maruoka, Shinji Kimura, Katsurnasa Watanabe

Research output: Contribution to journalArticle

4 Citations (Scopus)


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 optimization. This paper presents a satisfiability-based multi-cycle path detection method, where the detection problems are reduced to CNF formulae and 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 to ISCAS'89 benchmarks and other sample circuits. Experimental results show the remarkable improvements on the size of manipulatable circuits.

Original languageEnglish
Pages (from-to)2600-2607
Number of pages8
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
Issue number12
Publication statusPublished - 2000 Dec
Externally publishedYes


ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Hardware and Architecture
  • Information Systems

Cite this