Structural Coverage of Traversed Transitions for Symbolic Model Checking

スポンサーリンク

概要

• 論文の詳細を見る

• Coverage estimation for model checking has become an important issue in practical formal verification. Transition traversal coverage focuses on the transition characteristics of CTL operators and calculates which transitions are traversed during the model checking process of properties. One limitation of the method is the lack of the correspondence between the circuit structure and transitions. One transition might be covered no matter which part of the circuit is checked (or not) related to the transition. This leads to the overestimation of the coverability of properties. In this paper, we enhance the transition traversal coverage by analyzing the structural coverage of each traversed transition. We consider which variables are checked explicitly or implicitly on the traversed transitions. Thus, we deduce which part of the circuit is checked by properties for each traversed transition. The importance is that we can analyze which part of the circuit has not been verified. The accuracy of the transition traversal coverage is enhanced by our technique. We show the effectiveness of the proposed method by experiments.

• 2005-11-25

著者

• Kimura Shinji

  Graduate School Of Information Production And Systems Waseda University

• Kimura Shinji

  Graduate School Of Ips Waseda University

• XU Xingwen

  Graduate School of IPS, Waseda University

• HORIKAWA Kazunari

  System LSI Design Division, Toshiba Semiconductor

• TSUCHIYA Takehiko

  System LSI Design Division, Toshiba Semiconductor

• Tsuchiya Takehiko

  System Lsi Design Division Toshiba Semiconductor

• Xu Xingwen

  Graduate School Of Ips Waseda University

• Horikawa Kazunari

  System Lsi Design Division Toshiba Semiconductor

• Kimura Shinji

  Graduate School Of Engineering 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)
• 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設計技術)
• Finite Input-Memory Automaton Based Checker Synthesis of System Verilog Assertions for FPGA Prototyping
• _
• 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)
• 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)
• Look Up Table Compaction Based on Folding of Logic Functions(Special Section on VLSI Design and CAD Algorithms)
• 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
• RAY-SPACE CODING USING SINUSOIDAL STRUCTURE IN CIRCULAR CAMERA ARRANGEMENT(International Workshop on Advanced Image Technology 2006)
• 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
• Checker circuit generation for System Verilog Assertions in prototyping verification (システムLSI設計技術)
• Efficient Hybrid Grid Synthesis Method Based on Genetic Algorithm for Power/Ground Network Optimization with Dynamic Signal Consideration
• Automatic Multi-Stage Clock Gating Optimization Using ILP Formulation
• Multi-Operand Adder Synthesis Targeting FPGAs
• On Gate Level Power Optimization of Combinational Circuits Using Pseudo Power Gating
• Write Control Method for Nonvolatile Flip-Flops Based on State Transition Analysis
• An Exact Approach for GPC-Based Compressor Tree Synthesis
• Dual-Stage Pseudo Power Gating with Advanced Clustering Algorithm for Gate Level Power Optimization

もっと見る 閉じる

スポンサーリンク