{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:58:58Z","timestamp":1740131938203,"version":"3.37.3"},"reference-count":42,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"Intel Corporation at University of Florida"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput."],"published-print":{"date-parts":[[2024,1]]},"DOI":"10.1109\/tc.2023.3329243","type":"journal-article","created":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T18:54:03Z","timestamp":1699469643000},"page":"278-291","source":"Crossref","is-referenced-by-count":0,"title":["Correct-by-Construction Design of Custom Accelerator Microarchitectures"],"prefix":"10.1109","volume":"73","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4372-926X","authenticated-orcid":false,"given":"Jin","family":"Yang","sequence":"first","affiliation":[{"name":"Strategic CAD and Heterogenous Platform Lab, Intel Labs, Hillsboro, OR, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7567-2870","authenticated-orcid":false,"given":"Zhenkun","family":"Yang","sequence":"additional","affiliation":[{"name":"Strategic CAD and Heterogenous Platform Lab, Intel Labs, Hillsboro, OR, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0890-7673","authenticated-orcid":false,"given":"Jeremy","family":"Casas","sequence":"additional","affiliation":[{"name":"Strategic CAD and Heterogenous Platform Lab, Intel Labs, Hillsboro, OR, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8671-5052","authenticated-orcid":false,"given":"Sandip","family":"Ray","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Florida, Gainesville, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_33"},{"key":"ref2","first-page":"35","article-title":"A formal HDL and its use in the FM9001 verification","volume-title":"Mechanized Reasoning and Hardware Design, Prentice-Hall International Series in Computer Science","author":"Hunt","year":"1992"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_44"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014122630277"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_11"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_39"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0523-7_5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/52.57892"},{"key":"ref10","first-page":"349","article-title":"Formal verification of pipelines based on string-functional semantics","volume-title":"Formal VLSI Correctness Verification, VLSI Design Methods II","author":"Bronstein","year":"1990"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_3"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_40"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_40"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_33"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-6401-7_38-1"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_32"},{"issue":"9780","key":"ref17","first-page":"42","article-title":"End-to-end verification of arm processors with Isa-formal","volume-title":"Proc. Int. Conf. Comput. Aided Verification (CAV\u201916), Lecture Notes in Computer Science","volume":"9780","author":"Reid","year":"2016"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_10"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/40.768501"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_25"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/date.2010.5457049"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2013.6657090"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2006.4380828"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"ref27","article-title":"CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler","volume-title":"Proc. Embedded Real Time Softw. Syst. (ERTS)","author":"K\u00e4stner","year":"2018"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103709"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/358438.349314"},{"key":"ref31","article-title":"Stratus high-level synthesis"},{"key":"ref32","article-title":"Catapult high-level synthesis"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/HOTCHIPS.2019.8875657"},{"key":"ref34","article-title":"The intertwined history of DARPA and Moores law, DARPA 2018","volume-title":"Defense Media Network","author":"Chappell","year":"2018"},{"article-title":"Sandy bridge bug 2x costly as pentium math bug","volume-title":"Toms Hardware","year":"2011","key":"ref35"},{"article-title":"Intels sapphire rapids had 500 bugs, launch window moves further","volume-title":"Toms Hardware","year":"2022","key":"ref36"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/69624.357207"},{"volume-title":"Computer Architecture: A Quantitative Approach","year":"2011","author":"Hennessy","key":"ref40"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293910"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS54210.2022.00031"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/12\/10372122\/10312784.pdf?arnumber=10312784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T05:46:36Z","timestamp":1716443196000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10312784\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1]]},"references-count":42,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tc.2023.3329243","relation":{},"ISSN":["0018-9340","1557-9956","2326-3814"],"issn-type":[{"type":"print","value":"0018-9340"},{"type":"electronic","value":"1557-9956"},{"type":"electronic","value":"2326-3814"}],"subject":[],"published":{"date-parts":[[2024,1]]}}}