Guillaume Plassan
Abstract
During 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 creation of missing assumptions are a significant time burden. In this article, we present a methodology to automatically mine these missing assumptions from counter-examples. First, multiple counter-examples are generated for the same property. Then, relevant behaviors are mined from the counter-examples. Finally, corresponding assumptions are filtered and a small amount is returned to the user for review.
- Martín Abadi, Leslie Lamport, and Pierre Wolper. 1989. Realizable and unrealizable specifications of reactive systems. In ICALP’89. Springer, 1--17. Google Scholar
Digital Library
- Accellera. Open Verification Library (OVL). Retrieved April 2014 from http://accellera.org/activities/working-groups/ovl.Google Scholar
- Michele Bertasi, Giuseppe Di Guglielmo, and Graziano Pravadelli. 2013. Automatic generation of compact formal properties for effective error detection. In CODES+ISSS’13. IEEE, 1--10. Google ScholarDigital Library
- Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In TACAS’99. Springer, 193--207. Google ScholarDigital Library
- Robert K. Brayton and Alan Mishchenko. 2010. ABC: An academic industrial-strength verification tool. In CAV’10. Springer, 24--40. Google ScholarDigital Library
- Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. 2008. Environment assumptions for synthesis. In CONCUR. Springer, 147--161. Google ScholarDigital Library
- Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In CAV’00. Springer, 154--169. Google ScholarDigital Library
- A. Danese, T. Ghasempouri, and G. Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In DATE’15. ACM, 67--72. Google ScholarDigital Library
- Niklas Eén, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In FMCAD’11. FMCAD Inc., 125--134. Google ScholarDigital Library
- Shigeki Hagihara, Yusuke Kitamura, Masaya Shimakawa, and Naoki Yonezaki. 2009. Extracting environmental constraints to make reactive system specifications realizable. In APSEC’09. IEEE Computer Society, 61--68. Google ScholarDigital Library
- Haifa-IBM-Laboratories. IBM Generalized Buffer. Retrieved May 2017 from http://www.research.ibm.com/haifa/projects/verification/RB_Homepage/tutorial3/.Google Scholar
- Samuel Hertz, David Sheridan, and Shobha Vasudevan. 2013. Mining hardware assertions with guidance from static analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 32, 6 (2013), 952--965. Google ScholarDigital Library
- IEEE. 2010. IEEE standard for property specification language (PSL). IEEE Std 1850-2010 (April 2010), 1--182.Google Scholar
- IEEE. 2013. IEEE standard for SystemVerilog -- unified hardware design, specification, and verification language. IEEE Std 1800-2012 (Feb 2013), 1--1315.Google Scholar
- Brian Keng. 2013. Advances in Debug Automation for a Modern Verification Environment. Ph.D. Dissertation. University of Toronto, Toronto, Ontario.Google Scholar
- Brian Keng, Evean Qin, Andreas Veneris, and Bao Le. 2014. Automated debugging of missing assumptions. In Asia-Pacific DAC’14. IEEE Computer Society, 732--737.Google Scholar
- Wenchao Li, Lili Dworkin, and Sanjit A. Seshia. 2011. Mining assumptions for synthesis. In MEMOCODE’11. IEEE, 43--50. Google ScholarDigital Library
- Alan Mishchenko, Niklas Een, and Robert Brayton. 2013. A toolbox for counter-example analysis and optimization. In IWLS’13. IEEE. Retrieved from https://people.eecs.berkeley.edu/∼alanmi/publications/2013/iwls13_cex.pdf.Google Scholar
- Guillaume Plassan. 2018. Conclusive Formal Verification of Clock-Domain Crossing Properties. Ph.D. Dissertation. University of Grenoble Alpes, Grenoble, France.Google Scholar
- Guillaume Plassan, Katell Morin-Allory, and Dominique Borrione. 2017. Extraction of missing formal assumptions in under-constrained designs. In ACM-IEEE MEMOCODE’17. ACM, 94--103. Google ScholarDigital Library
- A. Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, 46--57. Google ScholarDigital Library
- R. K. Ranjan, C. Coelho, and S. Skalberg. 2009. Beyond verification: Leveraging formal for debugging. In DAC’09. ACM, 648--651. Google ScholarDigital Library
- University of Washington. The Daikon Invariant Detector. Retrieved May 2017 from http://plse.cs.washington.edu/daikon/.Google Scholar
- 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’10. IEEE Computer Society, 626--629. Google ScholarDigital Library
Index Terms
- Mining Missing Assumptions from Counter-Examples
Recommendations
Extraction of missing formal assumptions in under-constrained designs
MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System DesignIn 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 ...
Finding feasible abstract counter-examples
A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-...
Compositional verification by model checking for counter-examples
ISSTA '96: Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysisMany concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of ...
Comments