{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:18Z","timestamp":1750306518276,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,11,18]],"date-time":"2014-11-18T00:00:00Z","timestamp":1416268800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001868","name":"National Science Council Taiwan","doi-asserted-by":"publisher","award":["NSC101-2221-E-008-137-MY3 and NSC101-2628-E-009-012-MY2"],"award-info":[{"award-number":["NSC101-2221-E-008-137-MY3 and NSC101-2628-E-009-012-MY2"]}],"id":[{"id":"10.13039\/501100001868","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2014,11,18]]},"abstract":"<jats:p>\n            SystemVerilog provides powerful language constructs for verification, and one of them is the\n            <jats:italic>covergroup<\/jats:italic>\n            functional coverage model. This model is designed as a complement to assertion verification, that is, it has the advantage of defining cross-coverage over multiple coverage points. In this article, a coverage-driven verification (CDV) approach is formulated as a simultaneous Boolean satisfiability (SAT) problem that is based on covergroups. The coverage\n            <jats:italic>bins<\/jats:italic>\n            defined by the functional model are converted into Conjunction Normal Form (CNF) and then solved together by our proposed simultaneous SAT algorithm PLNSAT to generate stimuli for improving coverage. The basic PLNSAT algorithm is then extended in our second proposed algorithm GPLNSAT, which exploits additional information gleaned from the structure of SystemVerilog covergroups. Compared to generating stimuli separately, the simultaneous SAT approaches can share learned knowledge across each coverage target, thus reducing the overall solving time drastically. Experimental results on a UART circuit and the largest ITC benchmark circuits show that the proposed algorithms can achieve 10.8x speedup on average and outperform state-of-the-art techniques in most of the benchmarks.\n          <\/jats:p>","DOI":"10.1145\/2651400","type":"journal-article","created":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T15:29:41Z","timestamp":1416842981000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Coverage-Driven Stimulus Generation Using Simultaneous SAT Solving, with Application to SystemVerilog"],"prefix":"10.1145","volume":"20","author":[{"given":"An-Che","family":"Cheng","sequence":"first","affiliation":[{"name":"National Chiao Tung University, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chia-Chih (Jack)","family":"Yen","sequence":"additional","affiliation":[{"name":"Synopsys Taiwan Co., Ltd., Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Celina G.","family":"Val","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Bayless","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iris Hui-Ru","family":"Jiang","sequence":"additional","affiliation":[{"name":"National Chiao Tung University, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing-Yang","family":"Jou","sequence":"additional","affiliation":[{"name":"National Central University and National Chiao Tung University, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,11,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310108"},{"volume-title":"Emulation, Post-Fabrication Debugging and On-Line Monitoring","author":"Boul\u00e9 Marc","key":"e_1_2_1_2_1","unstructured":"Marc Boul\u00e9 and Zeljko Zilic . 2008. Generating Hardware Assertion Checkers: For Hardware Verification , Emulation, Post-Fabrication Debugging and On-Line Monitoring . Springer . Marc Boul\u00e9 and Zeljko Zilic. 2008. Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring. Springer."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763279"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2041846"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2011.49"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International High Level Design Validation, and Test Workshop (HLDVT'12)","author":"Cheng An-Che","year":"2012","unstructured":"An-Che Cheng , Chia-Chih Yen , and Jing-Yang Jou . 2012 . A formal method to improve system verilog functional coverage . In Proceedings of the International High Level Design Validation, and Test Workshop (HLDVT'12) . 56--63. An-Che Cheng, Chia-Chih Yen, and Jing-Yang Jou. 2012. A formal method to improve system verilog functional coverage. In Proceedings of the International High Level Design Validation, and Test Workshop (HLDVT'12). 56--63."},{"volume-title":"Proceedings of the Design, Automation and Test in Europe Conference (DATE'06)","author":"Das Sayantan","key":"e_1_2_1_7_1","unstructured":"Sayantan Das , Rizi Mohanty , Pallab Dasgupta , and Partha P. Chakrabarti . 2006. Synthesis of system verilog assertions . In Proceedings of the Design, Automation and Test in Europe Conference (DATE'06) . 1--6. Sayantan Das, Rizi Mohanty, Pallab Dasgupta, and Partha P. Chakrabarti. 2006. Synthesis of system verilog assertions. In Proceedings of the Design, Automation and Test in Europe Conference (DATE'06). 1--6."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10)","author":"E\u00e9n Niklas","year":"2010","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Nina Amla . 2010 . A single-instance incremental sat formulation of proof- and counterexample-based abstraction . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10) . 181--188. Niklas E\u00e9n, Alan Mishchenko, and Nina Amla. 2010. A single-instance incremental sat formulation of proof- and counterexample-based abstraction. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10). 181--188."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03)","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson . 2003 a. An extensible sat-solver . In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03) . 502--518. Niklas E\u00e9n and Niklas S\u00f6rensson. 2003a. An extensible sat-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03). 502--518."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1114283.1114497"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10)","author":"Franz\u00e9n Anders","year":"2010","unstructured":"Anders Franz\u00e9n , Alessandro Cimatti , Alexander Nadel , Roberto Sebastiani , and Jonathan Shalev . 2010 . Applying smt in symbolic execution of microcode . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10) . 121--128. Anders Franz\u00e9n, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, and Jonathan Shalev. 2010. Applying smt in symbolic execution of microcode. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'10). 121--128."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90018-C"},{"key":"e_1_2_1_14_1","volume-title":"IEEE standard for systemverilog--Unified hardware design, specification, and verification language","author":"Std IEEE","year":"1800","unstructured":"IEEE Std . 2013. IEEE standard for systemverilog--Unified hardware design, specification, and verification language . IEEE Std 1800 -2012 (revision of ieee std 1800-2009). 1--1315. http:\/\/dx.doi.org\/10.1109\/IEEESTD.2013.6469140. 10.1109\/IEEESTD.2013.6469140 IEEE Std. 2013. IEEE standard for systemverilog--Unified hardware design, specification, and verification language. IEEE Std 1800-2012 (revision of ieee std 1800-2009). 1--1315. http:\/\/dx.doi.org\/10.1109\/IEEESTD.2013.6469140."},{"volume-title":"ITC'99 benchmark homepage. http:\/\/www.cerc.utexas.edu\/itc99-benchmarks\/bench.html.","year":"1999","key":"e_1_2_1_15_1","unstructured":"ITC'99 Benchmark. 1999 . ITC'99 benchmark homepage. http:\/\/www.cerc.utexas.edu\/itc99-benchmarks\/bench.html. ITC'99 Benchmark. 1999. ITC'99 benchmark homepage. http:\/\/www.cerc.utexas.edu\/itc99-benchmarks\/bench.html."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.062"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS-EERC.2009.19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_9"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11678779_5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278500"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2492708.2492745"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"volume-title":"Proceedings of the 27th Annual International Symposium on Fault-Tolerant Computing (FTCS'97)","author":"Joao","key":"e_1_2_1_23_1","unstructured":"Joao P. Marques-Silva and Karem A. Sakallah. 1997. Robust search algorithms for test pattem generation . In Proceedings of the 27th Annual International Symposium on Fault-Tolerant Computing (FTCS'97) . 152--161. Joao P. Marques-Silva and Karem A. Sakallah. 1997. Robust search algorithms for test pattem generation. In Proceedings of the 27th Annual International Symposium on Fault-Tolerant Computing (FTCS'97). 152--161."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_26_1","unstructured":"MathSAT. 2013. The mathsat 5 smt solver. http:\/\/mathsat.fbk.eu\/.  MathSAT. 2013. The mathsat 5 smt solver. http:\/\/mathsat.fbk.eu\/."},{"key":"e_1_2_1_27_1","unstructured":"Mentor Graphics. 2013. Coverage cookbook. https:\/\/verificationacademy.com\/cookbook\/coverage.  Mentor Graphics. 2013. Coverage cookbook. https:\/\/verificationacademy.com\/cookbook\/coverage."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/367072.367119"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI.Design.2010.47"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2209291.2209297"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000004785.67232.f8"},{"volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"Tseitin Grigorii S.","key":"e_1_2_1_33_1","unstructured":"Grigorii S. Tseitin . 1970. On the complexity of derivation in propositional calculus . In Studies in Constructive Mathematics and Mathematical Logic, Part II , Consultants Bureau , 115--125. Grigorii S. Tseitin. 1970. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part II, Consultants Bureau, 115--125."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2008.53"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD'11)","author":"Wu Bo-Han","year":"2011","unstructured":"Bo-Han Wu , Chun-Ju Yang , Chia-Cheng Tso , and Chung-Yang (RIC) Huang . 2011 . Toward an extremely-high-throughput and even-distribution pattern generator for the constrained random simulation techniques . In Proceedings of the International Conference on Computer-Aided Design (ICCAD'11) 602--607. Bo-Han Wu, Chun-Ju Yang, Chia-Cheng Tso, and Chung-Yang (RIC) Huang. 2011. Toward an extremely-high-throughput and even-distribution pattern generator for the constrained random simulation techniques. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'11) 602--607."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2012.37"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2013.55"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 15th Asia and South Pacific Design Automation Conference (ASPDAC'10)","author":"Yeh Hu-Hsi","year":"2010","unstructured":"Hu-Hsi Yeh and Chung-Yang Huang . 2010 . Automatic constraint generation for guided random simulation . In Proceedings of the 15th Asia and South Pacific Design Automation Conference (ASPDAC'10) . 613--618. Hu-Hsi Yeh and Chung-Yang Huang. 2010. Automatic constraint generation for guided random simulation. In Proceedings of the 15th Asia and South Pacific Design Automation Conference (ASPDAC'10). 613--618."},{"key":"e_1_2_1_40_1","unstructured":"Jun Yuan Carl Pixley and Adnan Aziz. 2006. Constraint-Based Verification. Springer.   Jun Yuan Carl Pixley and Adnan Aziz. 2006. Constraint-Based Verification. Springer."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the National Conference on Artificial Intelligence. 155--160","author":"Zabih Ramin","year":"1988","unstructured":"Ramin Zabih and David Mcallester . 1988 . A rearrangement search strategy for determining propositional satisfiability . In Proceedings of the National Conference on Artificial Intelligence. 155--160 . Ramin Zabih and David Mcallester. 1988. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence. 155--160."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2651400","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2651400","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:11:54Z","timestamp":1750227114000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2651400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,18]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,11,18]]}},"alternative-id":["10.1145\/2651400"],"URL":"https:\/\/doi.org\/10.1145\/2651400","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2014,11,18]]},"assertion":[{"value":"2014-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}