Cited By
View all- Plassan GMorin-Allory KBorrione D(2019)Mining Missing Assumptions from Counter-ExamplesACM Transactions on Embedded Computing Systems10.1145/328875918:1(1-25)Online publication date: 25-Jan-2019
Extraction of missing formal assumptions in under-constrained designs
Pages 94 - 103
Abstract
In the context of the formal functional verification of RTL designs, experience shows that a false failure is often observed. Most of the time, this failure is cause d by an under-constrained model. The analysis of the root cause for the verification error and the creation of missing constraints are a significant time burden. In this paper, we present a methodology to automatically infer these missing constraints: Constraint Extraction from Counter-Examples (CExtract). First, multiple counter-examples are generated for the same property. Then, potential constraints are mined from the counter-examples, and filtered to provide a limited number of assumptions for the user for review.
References
[1]
2010. IEEE Standard for Property Specification Language (PSL).
[2]
Martín Abadi, Leslie Lamport, and Pierre Wolper. 1989. Realizable and unrealizable specifications of reactive systems. In ICALP. 1--17.
[3]
Accellera. Accessed April 2014. Open Verification Library (OVL). http://accellera.org/activities/working-groups/ovl
[4]
Michele Bertasi, Giuseppe Di Guglielmo, and Graziano Pravadelli. 2013. Automatic generation of compact formal properties for effective error detection. In CODES+ISSS. IEEE, 1--10.
[5]
Robert K. Brayton and Alan Mishchenko. 2010. ABC: An Academic Industrial-Strength Verification Tool. In CAV. 24--40.
[6]
Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann. 2008. Environment assumptions for synthesis. In CONCUR. 147--161.
[7]
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In CAV.
[8]
A. Danese, T. Ghasempouri, and G. Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In DATE. 67--72.
[9]
G. Fey and R. Dreschler. 2003. Finding good counter-examples to aid design verification. In MEMOCODE. 51--52.
[10]
Shigeki Hagihara, Yusuke Kitamura, Masaya Shimakawa, and Naoki Yonezaki. 2009. Extracting environmental constraints to make reactive system specifications realizable. In APSEC. 61--68.
[11]
Haifa-IBM-Laboratories. Accessed May, 2017. IBM Generalized Buffer. http://www.research.ibm.com/\haifa/projects/verification/RB_Homepage/tutorial3/
[12]
Samuel Hertz, David Sheridan, and Shobha Vasudevan. 2013. Mining hardware assertions with guidance from static analysis. IEEE Trans. on CAD 32, 6 (2013), 952--965.
[13]
Brian Keng. 2013. Advances in Debug Automation for a Modern Verification Environment. Ph.D. Dissertation. University of Toronto.
[14]
Brian Keng, Evean Qin, Andreas Veneris, and Bao Le. 2014. Automated Debugging of Missing Assumptions. In Asia-Pacific DAC. IEEE Computer Society, 732--737.
[15]
Wenchao Li, Lili Dworkin, and Sanjit A Seshia. 2011. Mining assumptions for synthesis. In MEMOCODE. 43--50.
[16]
Alan Mishchenko, Niklas Een, and Robert Brayton. 2013. A Toolbox for Counter-Example Analysis and Optimization. In IWLS.
[17]
Univ. of Washington. Accessed May, 2017. The Daikon Invariant Detector. http://plse.cs.washington.edu/daikon/
[18]
R. K. Ranjan, C. Coelho, and S. Skalberg. 2009. Beyond verification: Leveraging formal for debugging. In DAC. 648--651.
[19]
Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. Goldmine: Automatic assertion generation using data mining and static analysis. In DATE. 626--629.
Recommendations
Mining Missing Assumptions from Counter-Examples
Special Issue on MEMOCODE 2017 and Regular PapersDuring the formal functional verification of Register-Transfer Level designs, a false failure is often observed. Most of the time, this failure is caused by an underconstrained model. The analysis of the root cause for the verification error and the ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Formal Verification for Embedded System Designs
Embedded electronics today are becoming increasingly complex, which makes their design and analysis more and more difficult. In this paper, we focus on the formal verification of embedded system designs at multiple levels of abstraction, enabled by the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2017
192 pages
ISBN:9781450350938
DOI:10.1145/3127041
- General Chair:
- Jean-Pierre Talpin,
- Program Chairs:
- Patricia Derler,
- Klaus Schneider
Copyright © 2017 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 29 September 2017
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design
September 29 - October 2, 2017
Vienna, Austria
Acceptance Rates
MEMOCODE '17 Paper Acceptance Rate 22 of 48 submissions, 46%;
Overall Acceptance Rate 34 of 82 submissions, 41%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 66Total Downloads
- Downloads (Last 12 months)13
- Downloads (Last 6 weeks)2
Reflects downloads up to 30 Dec 2024
Other Metrics
Citations
Cited By
View all- Plassan GMorin-Allory KBorrione D(2019)Mining Missing Assumptions from Counter-ExamplesACM Transactions on Embedded Computing Systems10.1145/328875918:1(1-25)Online publication date: 25-Jan-2019
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in