{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,7,22]],"date-time":"2023-07-22T05:22:27Z","timestamp":1690003347299},"reference-count":39,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014,1]]},"DOI":"10.1109\/tcad.2013.2282776","type":"journal-article","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T18:53:48Z","timestamp":1388775228000},"page":"139-152","source":"Crossref","is-referenced-by-count":7,"title":["A High-Throughput and Arbitrary-Distribution Pattern Generator for the Constrained Random Verification"],"prefix":"10.1109","volume":"33","author":[{"given":"Bo-Han","family":"Wu","sequence":"first","affiliation":[]},{"given":"Chun-Ju","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Chung-Yang","family":"Huang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2429384.2429405"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2463209.2488880"},{"key":"ref33","first-page":"305","article-title":"On computing minimum unsatisfiable cores","author":"lynce","year":"2004","journal-title":"Proc 7th Int Conf Theory Applicat Satisfiability Test"},{"key":"ref32","article-title":"Extracting small unsatisfiable cores from unsatisfiable Boolean formula","author":"zhang","year":"2003","journal-title":"Proc 6th Int Conf Theory Applicat Satisfiability Test"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/28.5.530"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2011.6105392"},{"key":"ref36","year":"2010"},{"key":"ref35","first-page":"1027","article-title":"K-Means++: The advantages of careful seeding","author":"arthur","year":"2007","journal-title":"Proc 18th Annu ACM-SIAM Symp Discrete Algorithms"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1982.1056489"},{"key":"ref10","first-page":"71","article-title":"CalCS: SMT solving for non-linear convex constraints","author":"nuzzo","year":"2010","journal-title":"Proc FMCAD"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/CSCWD.2009.4968035"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2008.4484754"},{"key":"ref13","first-page":"769","article-title":"Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints","author":"deng","year":"2009","journal-title":"Proc ASPDAC"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/11499107_13","article-title":"On finding all minimally unsatisfiable subformulas","author":"liffiton","year":"2005","journal-title":"Proc Int Conf Theory Applicat Satisfiability Test"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF02243018"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2003.1270852"},{"key":"ref18","first-page":"670","article-title":"Towards efficient sampling: Exploiting random walk strategies","author":"wei","year":"2004","journal-title":"Proc Nat Conf Artif Intell"},{"key":"ref19","first-page":"521","article-title":"Local search strategies for satisfiability testing","author":"selman","year":"1993","journal-title":"Proc 2nd DIMACS Challenge Cliques Color Satisfiability"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1999.810715"},{"key":"ref28","first-page":"204","article-title":"Counting CSP solutions using generalized XOR constraints","author":"gomes","year":"2007","journal-title":"Proc 22nd Conf Artif Intell"},{"key":"ref3","year":"0"},{"key":"ref27","first-page":"481","article-title":"Near-uniform sampling of combinatorial spaces using XOR constraints","author":"gomes","year":"2006","journal-title":"Proc 20th Annu Conf Neural Inf Process Syst"},{"key":"ref6","first-page":"53","article-title":"Minisat v1. 13-A SAT solver with conflict-clause minimization","author":"sorensson","year":"2005","journal-title":"Proc SAT Competition"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.823348"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22196"},{"key":"ref8","first-page":"957","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"2009","journal-title":"Proc TACAS"},{"key":"ref7","year":"0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2012.6176425"},{"key":"ref9","first-page":"668","article-title":"Beaver: Engineering an efficient SMT solver for bit-vector arithmetic","author":"jha","year":"2009","journal-title":"Proc CAV"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.413.0386"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1063\/1.1699114"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_34"},{"key":"ref24","first-page":"441","article-title":"SAT vs. CSP","author":"walsh","year":"2000","journal-title":"Proc Int Conf Principles Prac Constraint Program"},{"key":"ref23","first-page":"487","article-title":"Application of formal word-level analysis to constrained random simulation","author":"kim","year":"2008","journal-title":"Proc CAV"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1143997.1144174"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF00116251"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/6685848\/06685865.pdf?arnumber=6685865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:28Z","timestamp":1638218428000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6685865\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":39,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2013.2282776","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1]]}}}