IEICE TRANSACTIONS on Fundamentals
Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion
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
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
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 -
English
