{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T06:00:17Z","timestamp":1763704817167},"reference-count":15,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1109\/date.2009.5090657","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T13:16:39Z","timestamp":1361279799000},"page":"196-201","source":"Crossref","is-referenced-by-count":30,"title":["Solver technology for system-level to RTL equivalence checking"],"prefix":"10.1109","author":[{"given":"A.","family":"Koelbl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Jacoby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Jain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Pixley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"Softfloat library","year":"0","key":"15"},{"journal-title":"A new interval approximation supporting bit operations and byte access","year":"2006","author":"backes","key":"13"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-27813-9_49","article-title":"cvc lite: a new implementation of the cooperating validity checker","author":"barrett","year":"2004","journal-title":"16th International Conference on Computer Aided Verification CAV'04"},{"year":"0","key":"11"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278530"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2005.1560201"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-005-8910-3"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"5","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1109\/ICCAD.1996.569607","article-title":"grasp - a new search algorithm for satisfiability","author":"marques-silva","year":"1996","journal-title":"Proceedings of IEEE\/ACM International Conference on Computer-Aided Design"},{"journal-title":"Minisat sat solver","year":"0","key":"4"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233663"},{"key":"8","first-page":"61","article-title":"effective preprocessing in sat through variable and clause elimination","author":"ee?n","year":"2005","journal-title":"SAT"}],"event":{"name":"2009 Design, Automation & Test in Europe Conference & Exhibition (DATE'09)","start":{"date-parts":[[2009,4,20]]},"location":"Nice","end":{"date-parts":[[2009,4,24]]}},"container-title":["2009 Design, Automation & Test in Europe Conference & Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4926138\/5090609\/05090657.pdf?arnumber=5090657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T03:48:20Z","timestamp":1498016900000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5090657\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":15,"URL":"https:\/\/doi.org\/10.1109\/date.2009.5090657","relation":{},"subject":[],"published":{"date-parts":[[2009,4]]}}}