{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T18:03:28Z","timestamp":1785953008999,"version":"3.56.0"},"reference-count":25,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,12,5]],"date-time":"2021-12-05T00:00:00Z","timestamp":1638662400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,12,5]]},"DOI":"10.1109\/dac18074.2021.9586090","type":"proceedings-article","created":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T23:30:34Z","timestamp":1636414234000},"page":"349-354","source":"Crossref","is-referenced-by-count":8,"title":["Property-driven Automatic Generation of Reduced-ISA Hardware"],"prefix":"10.1109","author":[{"given":"Nathan","family":"Bleier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Sartori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rakesh","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","author":"hus\u00e1r","year":"2016","journal-title":"Method and an apparatus for automatic processor design and verification"},{"key":"ref11","year":"2016","journal-title":"Desktop 3rd Generation Intel Core Processor Family"},{"key":"ref12","year":"2020","journal-title":"4th Generation Intel Core Procesor Family"},{"key":"ref13","article-title":"The risc-16 instruction-set architecture","author":"jacob","year":"2000","journal-title":"ENEE 446 Digital Computer Design"},{"key":"ref14","first-page":"657","article-title":"What good is temporal logic?","volume":"83","author":"lamport","year":"1983","journal-title":"IFIP Congress"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3060403.3060408"},{"key":"ref16","year":"2009","journal-title":"Cortex-M0 Technical Reference Manual"},{"key":"ref17","year":"2020","journal-title":"Arm custom instructions"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2872887.2750391"},{"key":"ref19","year":"2020","journal-title":"Ibex User Manual"},{"key":"ref4","article-title":"ARChitect Processor Configurator","year":"2014","journal-title":"Arc com Technical report"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1145\/1119772.1119831","article-title":"Hardware verification using ansi-c programs as a reference","author":"clarke","year":"2003","journal-title":"Proceedings of the ASP-DAC Asia and South Pacific Design Automation Conference 2003 ASPDAC"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/WWC.2001.990739"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/40.848473"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_24"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/HPCS.2018.00064"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080247"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2019.2897677"},{"key":"ref1","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref20","author":"lu?a?","year":"0","journal-title":"Bypassing kpti using the speculative behavior of the swapgs instruction"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/40.372360"},{"key":"ref21","author":"mashimo","year":"2017","journal-title":"Ridecore"},{"key":"ref24","volume":"116","author":"waterman","year":"2011","journal-title":"The Risc-v Instruction Set Manual Volume I Base User-level Isa"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2133375.2133377"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403670"}],"event":{"name":"2021 58th ACM\/IEEE Design Automation Conference (DAC)","location":"San Francisco, CA, USA","start":{"date-parts":[[2021,12,5]]},"end":{"date-parts":[[2021,12,9]]}},"container-title":["2021 58th ACM\/IEEE Design Automation Conference (DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9585997\/9586083\/09586090.pdf?arnumber=9586090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T16:55:52Z","timestamp":1652201752000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9586090\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,5]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/dac18074.2021.9586090","relation":{},"subject":[],"published":{"date-parts":[[2021,12,5]]}}}