| 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) |
| Page | pp. 1 - 6 |
| Keyword | model checking, properties completeness, transition coverage |
| 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. |
| PDF file |
| 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) |
| Page | pp. 19 - 24 |
| Keyword | Formal Verification, Register Transfer Level, Minimally Unsatisfiable Subsets |
| 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. |
| PDF file |
| 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) |
| Page | pp. 25 - 29 |
| Keyword | Shorter Error Sequence |
| 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. |
| PDF file |