Multi-Level Bounded Model Checking with Symbolic Counterexamples

スポンサーリンク

概要

• 論文の詳細を見る

• Bounded model checking is a widely used formal technique in both hardware and software verification. However, it cannot be applied if the bounds (number of time frames to be analyzed) become large, and deep bugs which are observed only through very long counter-examples cannot be detected. This paper presents a method concatenating multiple bounded model checking results efficiently with symbolic simulation. A bounded model checking with a large bound is recursively decomposed into multiple ones with smaller bounds, and symbolic simulation on each counterexample supports smooth connections to the others. A strong heuristic for the proposed method that targets deep bugs is also presented, and can be applied together with other efficient bounded model checking methods since it does not touch the basic bounded model checking algorithm.

著者

• FUJITA Masahiro

  VLSI Design and Education Center (VDEC), The University of Tokyo

• NISHIHARA Tasuku

  Department of Electronics Engineering, The University of Tokyo

• MATSUMOTO Takeshi

  VLSI Design and Education Center (VDEC), The University of Tokyo

関連論文

• Performance-Constrained Transistor Sizing for Different Cell Count Minimization
• AI-1-4 超ディペンダブルVLSIへの挑戦(AI-1.デイベンダブルVLSIに向けて,依頼シンポジウム,ソサイエティ企画)
• Synchronization Verification in System-Level Design with ILP Solvers(System Level Design,VLSI Design and CAD Algorithms)
• EFSM-based Weight-oriented Concolic Testing for Embedded Software
• Multi-Level Bounded Model Checking with Symbolic Counterexamples
• Low Power and Fault Tolerant Encoding Methods for On-Chip Data Transfer in Practical Applications(Low Power Methodology, VLSI Design and CAD Algorithms)
• Reducing scheduling overheads in dynamically reconfigurable processors (VLSI設計技術)
• Reducing scheduling overheads in dynamically reconfigurable processors (コンピュータシステム)
• Reducing scheduling overheads in dynamically reconfigurable processors (リコンフィギャラブルシステム)
• The AMS Extension to System Level Design Language-SpecC(System Level Design,VLSI Design and CAD Algorithms)
• Synchronization Mechanism for Timed/Untimed Mixed-Signal System Level Design Environment(Selected Papers from the 18th Workshop on Circuits and Systems in Karuizawa)
• Reducing scheduling overheads in Dynamically Reconfigurable Processors
• Reducing scheduling overheads in Dynamically Reconfigurable Processors
• Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath
• Interconnect-Aware Pipeline Synthesis for Array-Based Architectures
• Multi-Level Bounded Model Checking with Symbolic Counterexamples
• A Unified Framework for Equivalence Verification of Datapath Oriented Applications
• An Equivalence Checking Method for C Descriptions Based on Symbolic Simulation with Textual Differences(Simulation and Verification, VLSI Design and CAD Algorithms)
• An Automatic Method of Mapping I/O Sequences of Chip Execution onto High-level Design for Post-Silicon Debugging
• Data Flow Graph Partitioning Algorithms and Their Evaluations for Optimal Spatio-temporal Computation on a Coarse Grain Reconfigurable Architecture
• Performance Estimation with Automatic False-Path Detection for System-Level Designs
• Exact Minimum Factoring of Incompletely Specified Logic Functions via Quantified Boolean Satisfiability
• Custom Instruction Generation for Configurable Processors with Limited Numbers of Operands
• Trends in Formal Verification Techniques for C-based Hardware Designs

もっと見る 閉じる

スポンサーリンク