Sponsored By:
ASP-DAC 2006 Archives
1A-1
| Title | Transition-Based Coverage Estimation for Symbolic Model Checking |
| Author | *Xingwen Xu, Shinji Kimura (Graduate School of IPS, Waseda University, Japan), Kazunari Horikawa, Takehiko Tsuchiya (Toshiba Corporation Semiconductor Company, Japan) |
| Abstract | Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug. |
| Slides (pdf file) | 1A-1 |
1A-2
| Title | Word Level Functional Coverage Computation |
| Author | *Bijan Alizadeh (Microelectronic Research and Development Center of Iran, Iran) |
| Abstract | This paper proposes a word-level coverage metric to determine the completeness of a set of properties verified by a word-level method. An algorithm is presented to compute a functionality based coverage metric for a sequence property as specification. Control, intermediate and output signals are represented by a multiplexer based structure of linear integer equations, and RT level properties are directly applied to this representation. A set of integer equations are symbolically simulated based on the specified property in a predictable time. We used a canonical form of linear Taylor Expansion Diagram. |
| Slides (pdf file) | 1A-2 |
1A-3
| Title | Discovering the Input Assumptions in Specification Refinement Coverage |
| Author | Prasenjit Basu, Sayantan Das, *Pallab Dasgupta, Partha P Chakrabarti (Indian Institute of Technology Kharagpur, India) |
| Abstract | The design of a large chip is typically hierarchical -- large modules are recursively expanded into a collection of submodules. Each expansion refines the design due to the addition of level specific details. We believe that a similar approach is necessary to scale the capacity of formal property verification technology -- as the design gets refined from one level to another, the formal specification must also be refined to reflect the level specific design decisions. At the heart of this approach we propose a checker that identifies the input assumptions under which the refined specification "covers" the original specification. This enables the validation engineer to focus the verification effort on the remaining input scenarios thereby reducing the number of target coverage points for simulation. |
| Slides (pdf file) | 1A-3 |
1A-4
| Title | Refinement Strategies for Verification Methods Based on Datapath Abstraction |
| Author | *Zaher Semon Andraus, Mark Hammond Liffiton, Karem Ahmad Sakallah (The University of Michigan, Ann Arbor, United States) |
| Abstract | In this paper we explore the application of Counterexample Guided Abstraction Refinement (CEGAR) in the context of microprocessor correspondence checking. The approach is based on automatic datapath abstraction augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration. |
| Slides (pdf file) | 1A-4 |
1A-5
| Title | Generation of Shorter Sequences for High Resolution Error Diagnosis Using Sequential SAT |
| Author | Sung-Jui Pan, *Kwang-Ting Cheng (University of California, Santa Barbara, United States), John Moondanos, Ziyad Hanna (Intel Corporation, United States) |
| Abstract | Commonly used pattern sources in simulation-based verification include random, guided random, or design verification patterns. Although these patterns may help bring the design to those hard-to-reach states for activating the errors and for propagating them to observation points, they tend to be very long, which complicates the subsequent diagnosis process. As a key step in reducing the overall diagnosis complexity, we propose a method of generating a shorter error-sequence based on a given long error-sequence. We formulate the problem as a satisfiability problem and employ a SAT solver as the underlying engine for this task. By heuristically selecting an intermediate state $S_i$ which is reachable by the given long sequence, the task of finding the transfer sequence from the initial state to the target state can be divided into two easier tasks - finding a transfer sequence from the initial state to $S_i$ and one from $S_i$ to the target state. Our preliminary experimental results on public benchmark circuits show that the proposed method can achieve significant reduction in the length of the error sequences. |
| Slides (pdf file) | 1A-5 |