{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:07:49Z","timestamp":1761588469418,"version":"build-2065373602"},"reference-count":27,"publisher":"IBM","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IBM J. Res. & Dev."],"published-print":{"date-parts":[[2015,1]]},"DOI":"10.1147\/jrd.2014.2380271","type":"journal-article","created":{"date-parts":[[2015,2,2]],"date-time":"2015-02-02T15:20:16Z","timestamp":1422890416000},"page":"11:1-11:17","source":"Crossref","is-referenced-by-count":9,"title":["Solutions to IBM POWER8 verification challenges"],"prefix":"10.1147","volume":"59","author":[{"given":"K.-D.","family":"Schubert","sequence":"first","affiliation":[]},{"given":"J. M.","family":"Ludden","sequence":"additional","affiliation":[]},{"given":"S.","family":"Ayub","sequence":"additional","affiliation":[]},{"given":"J.","family":"Behrend","sequence":"additional","affiliation":[]},{"given":"B.","family":"Brock","sequence":"additional","affiliation":[]},{"given":"F.","family":"Copty","sequence":"additional","affiliation":[]},{"given":"S. M.","family":"German","sequence":"additional","affiliation":[]},{"given":"O.","family":"Hershkovitz","sequence":"additional","affiliation":[]},{"given":"H.","family":"Horbach","sequence":"additional","affiliation":[]},{"given":"J. R.","family":"Jackson","sequence":"additional","affiliation":[]},{"given":"K.","family":"Keuerleber","sequence":"additional","affiliation":[]},{"given":"J.","family":"Koesters","sequence":"additional","affiliation":[]},{"given":"L. S.","family":"Leitner","sequence":"additional","affiliation":[]},{"given":"G. B.","family":"Meil","sequence":"additional","affiliation":[]},{"given":"C.","family":"Meissner","sequence":"additional","affiliation":[]},{"given":"R.","family":"Morad","sequence":"additional","affiliation":[]},{"given":"A.","family":"Nahir","sequence":"additional","affiliation":[]},{"given":"V.","family":"Paruthi","sequence":"additional","affiliation":[]},{"given":"R. D.","family":"Peterson","sequence":"additional","affiliation":[]},{"given":"R. R.","family":"Pratt","sequence":"additional","affiliation":[]},{"given":"M.","family":"Rimon","sequence":"additional","affiliation":[]},{"given":"J. A.","family":"Schumann","sequence":"additional","affiliation":[]}],"member":"3082","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2014.2376132"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2011.2117370"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1147\/rd.461.0053"},{"key":"ref4","article-title":"Simulation-Driven Verification","volume-title":"Proc. DASS","author":"Bentley","year":"2009"},{"key":"ref5","first-page":"141","article-title":"Formal verification of error correcting circuits using computational algebraic \ngeometry","volume-title":"Proc. FMCAD","author":"Lvov","year":"2012"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.75"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2014.2380199"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2485922.2485942"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508263"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2004.1277900"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593241"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2002.1224444"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024913"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024916"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19583-9_15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2014.2380198"},{"key":"ref17","article-title":"Specification and verification of shared memory protocols and consistency models","volume-title":"Proc. Formal Methods Comput.-Aided Des.","author":"Chou","year":"2004"},{"key":"ref18","article-title":"Verifying cache coherence","volume-title":"Proc. EE Times","author":"Ranjan","year":"2011"},{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"ref19"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1992.276232"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1147\/rd.483.0347"},{"volume-title":"Breker Verification Systems","key":"ref22"},{"volume-title":"Technical Articles: Breker Verification Systems","key":"ref23"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2013.2279598"},{"issue":"5","key":"ref25","first-page":"18","article-title":"Caution: Clock crossing: A prescription for uncontaminated data across clock \ndomains","author":"Parker","year":"2004","journal-title":"Chip Des. Mag."},{"article-title":"Method, Apparatus, and Computer Program Product for Facilitating Modeling of a Combinatorial Logic \nGlitch at an Asynchronous Clock Domain Crossing","year":"2008","author":"Schuppe","key":"ref26"},{"article-title":"Method for Modeling Metastability Decay Through Latches in an Integrated Circuit \nModel","year":"2009","author":"Ja","key":"ref27"}],"container-title":["IBM Journal of Research and Development"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5288520\/7029148\/07029182.pdf?arnumber=7029182","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:03:13Z","timestamp":1761588193000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7029182\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1]]},"references-count":27,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1147\/jrd.2014.2380271","relation":{},"ISSN":["0018-8646","0018-8646"],"issn-type":[{"type":"print","value":"0018-8646"},{"type":"electronic","value":"0018-8646"}],"subject":[],"published":{"date-parts":[[2015,1]]}}}