{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:59:05Z","timestamp":1725749945225},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1109\/aspdac.2011.5722201","type":"proceedings-article","created":{"date-parts":[[2011,3,5]],"date-time":"2011-03-05T12:54:28Z","timestamp":1299329668000},"page":"293-296","source":"Crossref","is-referenced-by-count":7,"title":["Automatic formal verification of reconfigurable DSPs"],"prefix":"10.1109","author":[{"given":"Miroslav N.","family":"Velev","sequence":"first","affiliation":[]},{"given":"Ping","family":"Gao","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref33","DOI":"10.1109\/ASPDAC.2010.5419811"},{"doi-asserted-by":"publisher","key":"ref32","DOI":"10.1109\/HLDVT.2009.5340184"},{"doi-asserted-by":"publisher","key":"ref31","DOI":"10.1109\/ISQED.2006.142"},{"doi-asserted-by":"publisher","key":"ref30","DOI":"10.1504\/IJES.2005.008815"},{"doi-asserted-by":"publisher","key":"ref34","DOI":"10.1007\/978-3-642-16901-4_24"},{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1016\/S0890-5401(02)93175-5"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1109\/40.877948"},{"doi-asserted-by":"publisher","key":"ref12","DOI":"10.1007\/3-540-49519-3_3"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1145\/309847.309967"},{"key":"ref14","article-title":"Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic","author":"velev","year":"1999","journal-title":"Correct Hardware Design and Verification Methods LNCS 1703"},{"key":"ref15","article-title":"Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction","author":"velev","year":"2000","journal-title":"Design Automation Conference"},{"key":"ref16","article-title":"Formal Verification of VLIW Microprocessors with Speculative Execution","author":"veley","year":"2000","journal-title":"Computer-Aided Verification (CAV’00)"},{"key":"ref17","first-page":"252","article-title":"Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors","author":"velev","year":"2001","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’01)"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1016\/S0747-7171(02)00091-3"},{"key":"ref19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-45206-5_16","article-title":"Automatic Abstraction of Equations in a Logic of Equality","author":"velev","year":"2003","journal-title":"Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '03) LNAI 2796"},{"doi-asserted-by":"publisher","key":"ref28","DOI":"10.1109\/TE.2004.832880"},{"doi-asserted-by":"publisher","key":"ref4","DOI":"10.1145\/371282.371364"},{"doi-asserted-by":"publisher","key":"ref27","DOI":"10.1504\/IJES.2005.008815"},{"key":"ref3","article-title":"Tackling Functional Verification for Virtual Components","author":"anderson","year":"2000","journal-title":"ISD Magazine"},{"key":"ref6","article-title":"Automated Verification of Pipelined Microprocessor Control","author":"burch","year":"1994","journal-title":"Computer-Aided Verification (CAV '94) LNCS 818"},{"doi-asserted-by":"publisher","key":"ref29","DOI":"10.1007\/11560548_10"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1145\/566385.566390"},{"doi-asserted-by":"publisher","key":"ref8","DOI":"10.1109\/JSSC.2008.2007145"},{"key":"ref7","article-title":"Techniques for Verifying Superscalar Microprocessors","author":"burch","year":"1996","journal-title":"Design Automation Conference"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1007\/s10009-002-0087-0"},{"key":"ref9","article-title":"BDD Based Procedures for a Theory of Equality with Uninterpreted Functions","author":"goel","year":"1998","journal-title":"Computer-Aided Verification (CAV '98) LNCS 1427"},{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36126-X_8","article-title":"Relating Multi-Step and Single-Step Microprocessor Correctness Statements","author":"aagaard","year":"2002","journal-title":"Formal Methods in Computed Aided Design (FMCAD)"},{"key":"ref20","article-title":"Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-Solver When Formally Verifying Out-of-Order Processors","author":"velev","year":"2004","journal-title":"Artificial Intelligence and Mathematics (AI&MATH ’04)"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.1109\/ASPDAC.2004.1337588"},{"doi-asserted-by":"publisher","key":"ref21","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"ref24","article-title":"Encoding Global Unobservability for Efficient Translation to SAT","author":"velev","year":"2004","journal-title":"International Conference on Theory and Applications of Satisfiability Testing"},{"doi-asserted-by":"publisher","key":"ref23","DOI":"10.1109\/DATE.2004.1268859"},{"key":"ref26","article-title":"Comparison of Schemes for Encoding Unobservability in Translation to SAT","author":"velev","year":"2005","journal-title":"Asia and South Pacific Design Automation Conference (ASP-DAC"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1109\/ICCD.2004.1347910"}],"event":{"name":"2011 16th Asia and South Pacific Design Automation Conference ASP-DAC 2011","start":{"date-parts":[[2011,1,25]]},"location":"Yokohama, Japan","end":{"date-parts":[[2011,1,28]]}},"container-title":["16th Asia and South Pacific Design Automation Conference (ASP-DAC 2011)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5716646\/5722157\/05722201.pdf?arnumber=5722201","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T20:31:46Z","timestamp":1497904306000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5722201\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/aspdac.2011.5722201","relation":{},"subject":[],"published":{"date-parts":[[2011,1]]}}}