{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:53:06Z","timestamp":1725742386979},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2024,1,22]],"date-time":"2024-01-22T00:00:00Z","timestamp":1705881600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,1,22]],"date-time":"2024-01-22T00:00:00Z","timestamp":1705881600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,1,22]]},"DOI":"10.1109\/asp-dac58780.2024.10473912","type":"proceedings-article","created":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T19:06:53Z","timestamp":1711393613000},"page":"269-274","source":"Crossref","is-referenced-by-count":0,"title":["TIUP: Effective Processor Verification with Tautology-Induced Universal Properties"],"prefix":"10.1109","author":[{"given":"Yufeng","family":"Li","sequence":"first","affiliation":[{"name":"University of Chinese Academy of Sciences,Institute of Software, Chinese Academy of Sciences,Beijing,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiwei","family":"Ci","sequence":"additional","affiliation":[{"name":"University of Chinese Academy of Sciences,Institute of Software, Chinese Academy of Sciences,Beijing,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiusong","family":"Yang","sequence":"additional","affiliation":[{"name":"University of Chinese Academy of Sciences,Institute of Software, Chinese Academy of Sciences,Beijing,China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD45719.2019.8942096"},{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"ref2"},{"volume-title":"Model checking","year":"2018","author":"Clarke","key":"ref3"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"article-title":"Complete formal verification of tricore2 and other processors","volume-title":"Design and Verification Conference (DVCon)","author":"Bormann","key":"ref5"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_21"},{"volume-title":"Risc-v formal verification framework","year":"2018","author":"Wolf","key":"ref7"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542266"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"ref10","first-page":"351","article-title":"Ilang: a modeling and verification platform for socs using instruction-level abstractions","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I 25","author":"Huang"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2334301"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2015.7342397"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834401"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8341979"},{"key":"ref16","article-title":"Effective pre-silicon verification of processor cores by breaking the bounds of symbolic quick error detection","author":"Ganesan","year":"2021","journal-title":"arXiv preprint arXiv:2106.10392"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.23919\/DATE48585.2020.9116515"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SoC.2018.8644957"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715271"},{"volume-title":"Tautology. From MathWorld\u2014A Wolfram Web Resource","year":"2023","author":"Weisstein","key":"ref20"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"volume-title":"Yosys open synthesis suite","year":"2016","author":"Wolf","key":"ref22"},{"volume-title":"birisc-v - 32-bit dual issue risc-v cpu","year":"2021","key":"ref23"},{"volume-title":"Ridecore(risc-v dynamic execution core)","year":"2017","author":"Masashi Fujinami","key":"ref24"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00071"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_22"}],"event":{"name":"2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC)","start":{"date-parts":[[2024,1,22]]},"location":"Incheon, Korea, Republic of","end":{"date-parts":[[2024,1,25]]}},"container-title":["2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10473777\/10473787\/10473912.pdf?arnumber=10473912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T21:48:39Z","timestamp":1711489719000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10473912\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,22]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/asp-dac58780.2024.10473912","relation":{},"subject":[],"published":{"date-parts":[[2024,1,22]]}}}