{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T02:58:00Z","timestamp":1791341880911,"version":"4.3.1"},"reference-count":65,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2013,6,1]],"date-time":"2013-06-01T00:00:00Z","timestamp":1370044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1109\/tcad.2013.2241176","type":"journal-article","created":{"date-parts":[[2013,5,15]],"date-time":"2013-05-15T18:07:02Z","timestamp":1368641222000},"page":"952-965","source":"Crossref","is-referenced-by-count":81,"title":["Mining Hardware Assertions With Guidance From Static Analysis"],"prefix":"10.1109","volume":"32","author":[{"given":"S.","family":"Hertz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"D.","family":"Sheridan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Vasudevan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","first-page":"280","article-title":"Have I written enough properties?—A method of comparison between specification and implementation","author":"katz","year":"1999","journal-title":"Proc 10th IFIP WG 10 5 Adv Res Working Conf CHARME"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781330"},{"key":"ref33","first-page":"60","article-title":"Verifiying safety properties of a powerPC microprocessor using symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"Proc 11th Int Conf"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref31","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-48153-2_22","article-title":"Program slicing of hardware description languages","author":"clarke","year":"1999","journal-title":"Proc Correct Hardware Design Verification Methods"},{"key":"ref37","first-page":"1","article-title":"Towards coverage closure: Using GoldMine assertions for generating design validation stimulus","author":"liu","year":"2011","journal-title":"Proc DATE"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888997000015"},{"key":"ref35","author":"quinlan","year":"1993","journal-title":"C4 5 Programs for Machine Learning"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/BF00116251"},{"key":"ref60","year":"2013","journal-title":"Assertion Synthesis"},{"key":"ref62","author":"touhy","year":"2009"},{"key":"ref61","year":"2000"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/2429384.2429424"},{"key":"ref28","first-page":"60","article-title":"Verifiying safety properties of a powerPC microprocessor using symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"Proc 11th Int Conf CAV"},{"key":"ref64","first-page":"70","article-title":"Sat-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"Proc 12th Int Conf VMCAI"},{"key":"ref27","author":"edmund","year":"2000","journal-title":"Model checking"},{"key":"ref65","first-page":"24","article-title":"Abc: An academic industrial-strength verification tool","author":"brayton","year":"2010","journal-title":"Proc 22nd Int Conf CAV"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2007.38"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555774"},{"key":"ref22","author":"tan","year":"2005","journal-title":"Introduction to Data Mining"},{"key":"ref21","year":"0","journal-title":"Sun OpenSparc T2"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888905000408"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/775047.775053"},{"key":"ref26","volume":"lncs 5000","year":"2008","journal-title":"25 Years of Model Checking History Achievements Perspectives"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/69.553165"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/ATS.2005.30"},{"key":"ref51","first-page":"534","article-title":"Automatic generation of assertions for formal verification of PowerPC\/sup TM \/microprocessor arrays using symbolic trajectory evaluation","author":"wang","year":"1998","journal-title":"Proceedings 1998 Design and Automation Conference 35th DAC (Cat No 98CH36175) DAC"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970526"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2011.6081380"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2010.5419813"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2013995"},{"key":"ref55","author":"intent","year":"2013","journal-title":"Real Intent White Paper"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2008.4484908"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065786"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2005.6"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-61474-5_80","author":"bensalem","year":"1996","journal-title":"Computer-Aided Verification"},{"key":"ref11","first-page":"113","article-title":"A technique for invariant generation","author":"tiwari","year":"2001","journal-title":"Proc 7th Int Conf TACAS"},{"key":"ref40","first-page":"528","article-title":"Coverage metrics for temporal logic model checking","author":"chockler","year":"2001","journal-title":"Proc 7th Int Conf TACAS"},{"key":"ref12","first-page":"2989","article-title":"Verification of Java programs using symbolic execution and invariant generation","author":"pasareanu","year":"2004","journal-title":"Proc International SPIN Workshop on Model Checking of Software"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/996821.996832"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453150"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC.2006.19"},{"key":"ref17","author":"liu","year":"2011","journal-title":"Toward Coverage Closure Using GoldMine Assertions for Generating Design Validation Stimulus"},{"key":"ref18","year":"2006","journal-title":"IEEE Standard System C Language Reference Manual"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2010.5457129"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2005.1560217"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-9228-4"},{"key":"ref6","first-page":"131","article-title":"Assertion-based verification turns the corner","volume":"19","author":"gupta","year":"2002","journal-title":"IEEE Des Test"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1297666.1297670"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/566210.566213"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1120725.1120963"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2008.4484757"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808436"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2380445.2380481"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503275"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1137\/0206052"},{"key":"ref42","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s10009-004-0175-4","article-title":"Coverage metrics for formal verification","volume":"8","author":"chockler","year":"2006","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref41","first-page":"66","article-title":"A practical approach to coverage in model checking","author":"chockler","year":"2001","journal-title":"Proc 13th Int Conf CAV"},{"key":"ref44","author":"athavale","year":"2012","journal-title":"Coverage analysis for assertions and emulation based verification"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2008.53"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/6516595\/06516599.pdf?arnumber=6516599","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:25Z","timestamp":1638218425000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6516599\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6]]},"references-count":65,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2013.2241176","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6]]}}}