{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T06:06:49Z","timestamp":1729663609922,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,1]]},"DOI":"10.1109\/aspdac.2016.7428002","type":"proceedings-article","created":{"date-parts":[[2016,3,10]],"date-time":"2016-03-10T21:48:08Z","timestamp":1457646488000},"page":"139-146","source":"Crossref","is-referenced-by-count":4,"title":["Coupling reverse engineering and SAT to tackle NP-complete arithmetic circuitry verification in \u223cO(# of gates)"],"prefix":"10.1109","author":[{"given":"Yi","family":"Diao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xing","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tak-Kei","family":"Lam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Liang","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","article-title":"The effect of restarts on the efficiency of clause learning","author":"huang","year":"2007","journal-title":"IJCAI"},{"key":"ref11","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"2009","journal-title":"IJCAI"},{"key":"ref12","first-page":"466","article-title":"Equivalence checking hardware multiplier designs","volume":"1967","author":"jarvisalo","year":"1970","journal-title":"Papers on Computational Logic"},{"key":"ref13","article-title":"Satisfiability modulo theories","author":"biere","year":"2008","journal-title":"Handbook of Satisfiability"},{"key":"ref14","first-page":"46","article-title":"Implicit verification of structurally dissimilar arithmetic circuits","author":"stanion","year":"1999","journal-title":"Computer Design 1999 (ICCD '99) International Conference on"},{"doi-asserted-by":"publisher","key":"ref15","DOI":"10.1145\/370155.370315"},{"key":"ref16","first-page":"190","article-title":"Induction-based gate-level verification of multipliers","author":"chang","year":"2001","journal-title":"ICC 01"},{"doi-asserted-by":"publisher","key":"ref17","DOI":"10.1109\/ICCAD.2001.968616"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1109\/TCAD.2004.826548"},{"doi-asserted-by":"publisher","key":"ref19","DOI":"10.1109\/MEMCOD.2008.4547681"},{"key":"ref4","article-title":"Effective preprocessing in SAT through variable and clause elimination","author":"een","year":"2005","journal-title":"SAT"},{"year":"0","journal-title":"Easy-logic Technology Ltd","article-title":"Easy-LEC (25th Oct, 2014 version)","key":"ref27"},{"key":"ref3","first-page":"2","article-title":"*PHDD: an efficient graph representation for floating point circuit verification","author":"chen","year":"1997","journal-title":"Computer-Aided Design 1997 Digest of Technical Papers 1997 IEEE\/ACM International Conference on"},{"key":"ref6","first-page":"502","article-title":"An extensible SAT-solver","author":"een","year":"2003","journal-title":"Proc SAT"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"ref8","first-page":"51","article-title":"Lingeling, plingeling and treengeling entering the SAT competition 2013","author":"biere","year":"2013","journal-title":"Proc SAT Competition"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1007\/978-3-642-39071-5_23"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1145\/217474.217583"},{"doi-asserted-by":"publisher","key":"ref9","DOI":"10.1109\/DAC.2001.156196"},{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"publisher","key":"ref20","DOI":"10.1145\/1403375.1403575"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.1145\/2744769.2744925"},{"key":"ref21","first-page":"67","article-title":"Algebraic approach to arithmetic design verification","author":"basith","year":"2011","journal-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design"},{"doi-asserted-by":"publisher","key":"ref24","DOI":"10.7873\/DATE.2015.0746"},{"key":"ref23","article-title":"Orthogonal greedy coupling – a new optimization approach to 2-d fpga routing","author":"wu","year":"1995","journal-title":"Proc Design Automation Conference"},{"key":"ref26","article-title":"ICCAD-2014 CAD contest in simultaneous CNF encoder optimization with SAT solver setting selection","author":"hsu","year":"2014","journal-title":"Proc International Conference on Computer-Aided Design"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1109\/TETC.2013.2294918"}],"event":{"name":"2016 21st Asia and South Pacific Design Automation Conference (ASP-DAC)","start":{"date-parts":[[2016,1,25]]},"location":"Macao, Macao","end":{"date-parts":[[2016,1,28]]}},"container-title":["2016 21st Asia and South Pacific Design Automation Conference (ASP-DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7422345\/7427971\/7428002.pdf?arnumber=7428002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,30]],"date-time":"2016-09-30T01:32:37Z","timestamp":1475199157000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7428002\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/aspdac.2016.7428002","relation":{},"subject":[],"published":{"date-parts":[[2016,1]]}}}