Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion

Kazuhiro NAKAMURA; Shinji MARUOKA; Shinji KIMURA; Katsumasa WATANABE

Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion

Kazuhiro NAKAMURA, Shinji MARUOKA, Shinji KIMURA, Katsumasa WATANABE

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E83-A No.12 pp.2600-2607

Publication Date: 2000/12/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)

Category: Test

Cite this

Copy

Kazuhiro NAKAMURA, Shinji MARUOKA, Shinji KIMURA, Katsumasa WATANABE, "Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion" in IEICE TRANSACTIONS on Fundamentals, vol. E83-A, no. 12, pp. 2600-2607, December 2000, doi: .
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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e83-a_12_2600/_p

Copy

@ARTICLE{e83-a_12_2600,
author={Kazuhiro NAKAMURA, Shinji MARUOKA, Shinji KIMURA, Katsumasa WATANABE, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion},
year={2000},
volume={E83-A},
number={12},
pages={2600-2607},
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.},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2600
EP - 2607
AU - Kazuhiro NAKAMURA
AU - Shinji MARUOKA
AU - Shinji KIMURA
AU - Katsumasa WATANABE
PY - 2000
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E83-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2000
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.
ER -