Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion (Special Section on VLSI Design and CAD Algorithms)
スポンサーリンク
概要
- 論文の詳細を見る
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.
- 社団法人電子情報通信学会の論文
- 2000-12-25
著者
-
NAKAMURA Kazuhiro
the Graduate School of Information Science, Nara Institute of Science and Technology
-
KIMURA Shinji
the Graduate School of Information Science, Nara Institute of Science and Technology
-
WATANABE Katsumasa
the Graduate School of Information Science, Nara Institute of Science and Technology
-
Kimura Shinji
Graduate School Of Information Production And Systems Waseda University
-
Kimura S
Waseda Univ. Kitakyushu‐shi Jpn
-
WATANABE Kaoru
The author is with Osaka Electro-Communication University
-
Watanabe Katsumasa
The Graduate School Of Information Science Nara Institute Of Science And Technology
-
Nakamura Kazuhiro
The Graduate School Of Information Science Nara Institute Of Science And Technology
-
Watanabe K
Graduate School Of Information Science Nara Institute Of Science And Technology
-
MARUOKA Shinji
the Graduate School of Information Science, Nara Institute of Science and Technology
-
Maruoka Shinji
The Graduate School Of Information Science Nara Institute Of Science And Technology
-
Nakamura K
Takasago Research & Development Center Mitsubishi Heavy Industries Ltd.
-
Kohara Shunitsu
Department Of Computer Science Waseda University
-
Kimura Shinji
The Graduate School Of Information Science Advanced Institute Of Science And Technology
-
Nakamura Kazuhiro
The Graduate School Of Information Science Nagoya University
関連論文
- Exact Minimization of Free BDDs and Its Application to Pass-Transistor Logic Optimization (Special Section on VLSI Design and CAD Algorithms)
- Hardware Synthesis from C Programs with Estimation of Bit Length of Variables (Special Section on VLSI Design and CAD Algorithms)
- Timing Verification of Sequential Logic Circuits Based on Controlled Multi-Clock Path Analysis (Special Section on VLSI Design and CAD Algorithms)
- Selective Low-Care Coding : A Means for Test Data Compression in Circuits with Multiple Scan Chains(Selected Papers from the 18th Workshop on Circuits and Systems in Karuizawa)
- A Scheduling Problem in Multihop Networks
- The p-Collection Problem in a Flow Network with Lower Bounds (Special Section on Discrete Mathematics and Its Applications)
- The Optimal Architecture Design of Two-Dimension Matrix Multiplication Jumping Systolic Array
- Fine-Grained Power Gating Based on the Controlling Value of Logic Elements
- Fine-grained power gating based on the controlling value of logic gates (VLSI設計技術)
- Fine-grained power gating based on the controlling value of logic gates (システムLSI設計技術)
- Covering Problems in the p-Collection Problems
- The Problem of where to Locate p-Sinks in a Flow Network: Complexity Approach
- Realization Problems of a Tree with a Transmission Number Sequence (Special Section on the 6th Karuizawa Workshop on Circuits and Systems)
- Issue Mechanism for Embedded Simultaneous Multithreading Processor
- Multi-Cycle Path Detection Based on Propositional Satisfiability with CNF Simplification Using Adaptive Variable Insertion (Special Section on VLSI Design and CAD Algorithms)
- Sensitivity Analysis for Thermal Stress and Creep Problems
- Finite Element Analysis for Large Deformation Frictional Contact Problems with Finite Sliding
- Crack Initiating Limit for Cladding Tubes of PWR RCCA Rodlets Subject to Absorber Swelling
- Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High-Level Synthesis(Logic and High Synthesis)(VLSI Design and CAD Algorithms)
- A CMOS Rail-to-Rail Current Conveyer and Its Applications to Current-Mode Filters(Special Section on Papers Selected from ITC-CSCC 2002)
- A CMOS Rail-to-Rail Current Conveyor
- Look Up Table Compaction Based on Folding of Logic Functions(Special Section on VLSI Design and CAD Algorithms)
- Class A CMOS Current Conveyors
- A Clock-Feedthrough Compensated Switched-Current Memory Cell
- Irradiation Assisted Mechanical Cracking on Cladding Tubes of Control Rods in Nuclear Reactors
- Life Time Estimation for Cladding Tube Cracking Caused by Absorber Swelling of PWR RCCA Rodlets
- A Built-in Reseeding Technique for LFSR-Based Test Pattern Generation(Timing Verification and Test Generation)(VLSI Design and CAD Algorithms)
- A Built-in Reseeding Technique for LFSR-Based Test Pattern Generation
- Bit-Length Optimization Method for High-Level Synthesis Based on Non-linear Programming Technique(System Level Design,VLSI Design and CAD Algorithms)
- A Selective Scan Chain Reconfiguration through Run-Length Coding for Test Data Compression and Scan Power Reduction(Test)(VLSI Design and CAD Algorithms)
- A Hybrid Dictionary Test Data Compression for Multiscan-Based Designs(Test)(VLSI Design and CAD Algorithms)
- Unified Dual-Radix Architecture for Scalable Montgomery Multiplications in GF(P) and GF(2^n)
- Optimizing Controlling-Value-Based Power Gating with Gate Count and Switching Activity
- Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification(Simulation and Verification,VLSI Design and CAD Algorithms)
- Structural Coverage of Traversed Transitions for Symbolic Model Checking
- Structural Coverage of Traversed Transitions for Symbolic Model Checking
- Structural Coverage of Traversed Transitions for Symbolic Model Checking
- Structural Coverage of Traversed Transitions for Symbolic Model Checking
- Power Optimization of Sequential Circuits Using Switching Activity Based Clock Gating
- Automatic Generation of Java-Based, Database-Independent Query API
- Automatic Generation of Java-Based, Database-Independent Query API
- Checker circuit generation for System Verilog Assertions in prototyping verification (システムLSI設計技術)
- Robust Heuristics for Multi-Level Logic Simplification Considering Local Circuit Structure (Special Section on VLSI Design and CAD Algorithms)
- Preciseness of Discrete Time Verification (Special Section on VLSI Design and CAD Algorithms)
- Efficient Hybrid Grid Synthesis Method Based on Genetic Algorithm for Power/Ground Network Optimization with Dynamic Signal Consideration
- A VLSI Architecture with Multiple Fast Store-Based Block Parallel Processing for Output Probability and Likelihood Score Computations in HMM-Based Isolated Word Recognition
- Automatic Multi-Stage Clock Gating Optimization Using ILP Formulation
- Fine Grain Power Gating Based on Controllability Propagation and Power-off Probability
- Fine Grain Power Gating Based on Controllability Propagation and Power-off Probability
- Fine Grain Power Gating Based on Controllability Propagation and Power-off Probability
- Fine Grain Power Gating Based on Controllability Propagation and Power-off Probability