{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,14]],"date-time":"2026-09-14T05:39:19Z","timestamp":1789364359728,"version":"build-2803163510"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T00:00:00Z","timestamp":1548374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3288759","type":"journal-article","created":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T14:01:39Z","timestamp":1548684099000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Mining Missing Assumptions from Counter-Examples"],"prefix":"10.1145","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0124-9708","authenticated-orcid":false,"given":"Guillaume","family":"Plassan","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Grenoble INP, TIMA Laboratory, Grenoble Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Katell","family":"Morin-Allory","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Grenoble INP, TIMA Laboratory, Grenoble Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominique","family":"Borrione","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Grenoble INP, TIMA Laboratory, Grenoble Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"ICALP\u201989","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi , Leslie Lamport , and Pierre Wolper . 1989. Realizable and unrealizable specifications of reactive systems . In ICALP\u201989 . Springer , 1--17. Mart\u00edn Abadi, Leslie Lamport, and Pierre Wolper. 1989. Realizable and unrealizable specifications of reactive systems. In ICALP\u201989. Springer, 1--17."},{"key":"e_1_2_1_2_1","volume-title":"Open Verification Library (OVL). Retrieved","year":"2014","unstructured":"Accellera. Open Verification Library (OVL). Retrieved April 2014 from http:\/\/accellera.org\/activities\/working-groups\/ovl. Accellera. Open Verification Library (OVL). Retrieved April 2014 from http:\/\/accellera.org\/activities\/working-groups\/ovl."},{"key":"e_1_2_1_3_1","volume-title":"Giuseppe Di Guglielmo, and Graziano Pravadelli","author":"Bertasi Michele","year":"2013","unstructured":"Michele Bertasi , Giuseppe Di Guglielmo, and Graziano Pravadelli . 2013 . Automatic generation of compact formal properties for effective error detection. In CODES+ISSS\u201913. IEEE , 1--10. Michele Bertasi, Giuseppe Di Guglielmo, and Graziano Pravadelli. 2013. Automatic generation of compact formal properties for effective error detection. In CODES+ISSS\u201913. IEEE, 1--10."},{"key":"e_1_2_1_4_1","volume-title":"TACAS\u201999","author":"Biere Armin","unstructured":"Armin Biere , Alessandro Cimatti , Edmund M. Clarke , and Yunshan Zhu . 1999. Symbolic model checking without BDDs . In TACAS\u201999 . Springer , 193--207. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In TACAS\u201999. Springer, 193--207."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"A. Danese T. Ghasempouri and G. Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In DATE\u201915. ACM 67--72.   A. Danese T. Ghasempouri and G. Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In DATE\u201915. ACM 67--72.","DOI":"10.7873\/DATE.2015.0110"},{"key":"e_1_2_1_9_1","volume-title":"Brayton","author":"E\u00e9n Niklas","year":"2011","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Robert K . Brayton . 2011 . Efficient implementation of property directed reachability. In FMCAD\u201911. FMCAD Inc ., 125--134. Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In FMCAD\u201911. FMCAD Inc., 125--134."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2009.70"},{"key":"e_1_2_1_11_1","volume-title":"IBM Generalized Buffer. Retrieved","year":"2017","unstructured":"Haifa-IBM-Laboratories. IBM Generalized Buffer. Retrieved May 2017 from http:\/\/www.research.ibm.com\/haifa\/projects\/verification\/RB_Homepage\/tutorial3\/. Haifa-IBM-Laboratories. IBM Generalized Buffer. Retrieved May 2017 from http:\/\/www.research.ibm.com\/haifa\/projects\/verification\/RB_Homepage\/tutorial3\/."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2241176"},{"key":"e_1_2_1_13_1","volume-title":"IEEE standard for property specification language (PSL)","author":"IEEE.","year":"1850","unstructured":"IEEE. 2010. IEEE standard for property specification language (PSL) . IEEE Std 1850 -2010 (April 2010), 1--182. IEEE. 2010. IEEE standard for property specification language (PSL). IEEE Std 1850-2010 (April 2010), 1--182."},{"key":"e_1_2_1_14_1","volume-title":"IEEE standard for SystemVerilog -- unified hardware design, specification, and verification language","author":"IEEE.","year":"1800","unstructured":"IEEE. 2013. IEEE standard for SystemVerilog -- unified hardware design, specification, and verification language . IEEE Std 1800 -2012 (Feb 2013), 1--1315. IEEE. 2013. IEEE standard for SystemVerilog -- unified hardware design, specification, and verification language. IEEE Std 1800-2012 (Feb 2013), 1--1315."},{"key":"e_1_2_1_16_1","volume-title":"Asia-Pacific DAC\u201914","author":"Keng Brian","unstructured":"Brian Keng , Evean Qin , Andreas Veneris , and Bao Le. 2014. Automated debugging of missing assumptions . In Asia-Pacific DAC\u201914 . IEEE Computer Society , 732--737. Brian Keng, Evean Qin, Andreas Veneris, and Bao Le. 2014. Automated debugging of missing assumptions. In Asia-Pacific DAC\u201914. IEEE Computer Society, 732--737."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"e_1_2_1_18_1","volume-title":"IWLS\u201913","author":"Mishchenko Alan","year":"2013","unstructured":"Alan Mishchenko , Niklas Een , and Robert Brayton . 2013. A toolbox for counter-example analysis and optimization . In IWLS\u201913 . IEEE. Retrieved from https:\/\/people.eecs.berkeley.edu\/&sim;alanmi\/publications\/ 2013 \/iwls13_cex.pdf. Alan Mishchenko, Niklas Een, and Robert Brayton. 2013. A toolbox for counter-example analysis and optimization. In IWLS\u201913. IEEE. Retrieved from https:\/\/people.eecs.berkeley.edu\/&sim;alanmi\/publications\/2013\/iwls13_cex.pdf."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127046"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630082"},{"key":"e_1_2_1_23_1","volume-title":"The Daikon Invariant Detector. Retrieved","author":"University of Washington.","year":"2017","unstructured":"University of Washington. The Daikon Invariant Detector. Retrieved May 2017 from http:\/\/plse.cs.washington.edu\/daikon\/. University of Washington. The Daikon Invariant Detector. Retrieved May 2017 from http:\/\/plse.cs.washington.edu\/daikon\/."},{"key":"e_1_2_1_24_1","volume-title":"Goldmine: Automatic assertion generation using data mining and static analysis. In DATE\u201910","author":"Vasudevan Shobha","year":"2010","unstructured":"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\u201910 . IEEE Computer Society , 626--629. 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\u201910. IEEE Computer Society, 626--629."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3288759","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3288759","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:23Z","timestamp":1750208543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3288759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,25]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3288759"],"URL":"https:\/\/doi.org\/10.1145\/3288759","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,25]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}