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)

Abstract

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
VolumeE83-A
Issue number12
Publication statusPublished - 2000 Dec
Externally publishedYes

Fingerprint

Simplification
Insertion
Cycle
Path
Networks (circuits)
Clocks
Timing
Heuristics
Logic
Benchmark
Optimization
Experimental Results

ASJC Scopus subject areas

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

Cite this

Multi-cycle path detection based on propositional satisfiability with CNF simplification using adaptive variable insertion. / Nakamura, Kazuhiro; Maruoka, Shinji; Kimura, Shinji; Watanabe, Katsurnasa.

In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E83-A, No. 12, 12.2000, p. 2600-2607.

Research output: Contribution to journalArticle

@article{803840d1907440a9b8ee4a8ddd5644c6,
title = "Multi-cycle path detection based on propositional satisfiability with CNF simplification using adaptive variable insertion",
abstract = "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.",
author = "Kazuhiro Nakamura and Shinji Maruoka and Shinji Kimura and Katsurnasa Watanabe",
year = "2000",
month = "12",
language = "English",
volume = "E83-A",
pages = "2600--2607",
journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
issn = "0916-8508",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "12",

}

TY - JOUR

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

AU - Nakamura, Kazuhiro

AU - Maruoka, Shinji

AU - Kimura, Shinji

AU - Watanabe, Katsurnasa

PY - 2000/12

Y1 - 2000/12

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0034516553&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034516553&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0034516553

VL - E83-A

SP - 2600

EP - 2607

JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

SN - 0916-8508

IS - 12

ER -