Name
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/ASPDAC.2014.6742977 | Design Automation Conference |
Keywords | Field | DocType |
computer debugging,formal verification,OpenCores designs,RTL debugging,assertion debugging,automated missing assumption debugging,corner case design bug detection,debug automation,failure detection,fixed cycle assumptions,formal verification,function extraction,multiple formal counter-example generation | Programming language,Debug menu,Computer science,Assertion,Automation,Real-time computing,OpenCores,Corner case,Algorithmic program debugging,Debugging,Formal verification | Conference |
ISSN | Citations | PageRank |
2153-6961 | 3 | 0.42 |
References | Authors | |
10 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Brian Keng | 1 | 46 | 6.00 |
| Evean Qin | 2 | 3 | 0.42 |
| A. Veneris | 3 | 937 | 67.52 |
| Bao Le | 4 | 24 | 4.14 |