| Title | Automated Debugging of Missing Assumptions |
| Author | Brian Keng (University of Toronto, Canada), Evean Qin (Vennsa Technologies Inc., Canada), *Andreas Veneris, Bao Le (University of Toronto, Canada) |
| Page | pp. 732 - 737 |
| Keyword | Debugging, Assumptions, Verification, Formal |
| Abstract | Formal verification has increased efficiency by detecting
corner case design bugs but it has also introduced new
challenges when failures are detected. Once a counter-example is
returned by a formal tool, the user typically does not know if the
failure is caused by a design bug, an incorrectly written assertion,
or a missing assumption. Previous work in debug automation
has focused on the former two cases. This paper introduces a
novel methodology to automatically debug missing assumptions.
It begins by generating multiple formal counter-examples for the
error. Next, a function is extracted from these counter-examples
that encodes the input combinations that cause the assertion
to fail. This function is later used to generate a list of fixed
cycle assumptions that prevent failures similar to the generated
counter-examples. These filtered assumptions can then be used
as hints for the actual missing assumption. Further, if a missing
assumption is not the cause of the failure, the method offers the
additional benefit that the counter-examples it generates can be
utilized to debug the RTL and/or the assertion. An extensive set of
experimental results on OpenCores designs and assertions show
that the number of generated assumptions can be reduced by an
average of 38% using ten counter-examples, while an average of
28 assumptions is returned to the user. |
| Slides |
| Title | Property Directed Reachability for QF_BV with Mixed Type Atomic Reasoning Units |
| Author | *Tobias Welp (University of California, Berkeley, U.S.A.), Andreas Kuehlmann (Coverity, Inc./University of California, Berkeley, U.S.A.) |
| Page | pp. 738 - 743 |
| Keyword | IC3, PDR, Model Checking, QF_BV |
| Abstract | A generalization of Property Directed Reachability (PDR) for the theory QF_BV presented at DATE 2013 outperforms the original formulation if the required inductive invariant can be represented efficiently as a set of polytopes. However, many QF_BV model checking instances do not belong in this class and can be solved quickly with the original PDR algorithm. In this paper, we present a hybrid approach which uses both polytopes and Boolean cubes as atomic reasoning units combining the advantages of either homogeneous approach. We discuss theoretic properties of the presented algorithm and report experimental results demonstrating its effectiveness. |
| Slides |
| Title | Adaptive Interpolation-Based Model Checking |
| Author | *Chien-Yu Lai, Cheng-Yin Wu, Chung-Yan (Ric) Huang (National Taiwan University, Taiwan) |
| Page | pp. 744 - 749 |
| Keyword | interpolation, model checking, formal verification |
| Abstract | Interpolation-based model checking (IMC) is an important technique in modern formal verification tools. In essence, it relies on an abstraction and refinement process to derive an adequate image approximation for the reachability analysis. However, previous IMC algorithms only offer fixed degrees of abstraction and thus may fail in the proofs if the abstraction is too coarse- or fine-grained. In this paper, we propose an adaptive interpolation-based model checking algorithm in which the degree of abstraction can be adjusted on demand. That is, during the proof process, we closely monitor the effectiveness of the interpolation-based over-approximated image computation and thus adjust the degree of abstraction for the best performance. The experimental results confirm that our flexible interpolation indeed leads to an adequate degree of abstraction as our IMC algorithm outperforms previous ones in various aspects. |
| Slides |
| Title | Efficient Parallel GPU Algorithms for BDD Manipulation |
| Author | *Miroslav Velev, Ping Gao (Aries Design Automation, U.S.A.) |
| Page | pp. 750 - 755 |
| Keyword | Binary Decision Diagrams, Boolean Satisfiability, Formal Verification, GPU, Parallel Execution |
| Abstract | We present parallel algorithms for Binary Decision Diagram (BDD) manipulation optimized for efficient execution on Graphics Processing Units (GPUs). Compared to a sequential CPU-based BDD package with the same capabilities, our GPU implementation achieves at least 5 orders of magnitude speedup. To the best of our knowledge, this is the first work on using GPUs to accelerate a BDD package. |