{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T01:52:47Z","timestamp":1729648367325,"version":"3.28.0"},"reference-count":46,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,3]]},"DOI":"10.1109\/isqed.2014.6783383","type":"proceedings-article","created":{"date-parts":[[2014,4,16]],"date-time":"2014-04-16T17:24:16Z","timestamp":1397669056000},"page":"611-617","source":"Crossref","is-referenced-by-count":2,"title":["Formal verification of safety of polymorphic heterogeneous multi-core architectures"],"prefix":"10.1109","author":[{"given":"Miroslav N.","family":"Velev","sequence":"first","affiliation":[]},{"given":"Ping","family":"Gao","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"Siege SAT Solver V 4","year":"0","author":"ryan","key":"19"},{"key":"35","article-title":"Formal verification of pipelined microprocessors by correspondence checking ph d thesis","author":"velev","year":"2004","journal-title":"Department of Electrical and Computer Engineering"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93175-5"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2004.1347910"},{"key":"18","article-title":"Bahurupi: A polymorphic heterogeneous multi-core architecture acm","volume":"8","author":"pricopi","year":"2012","journal-title":"Transactions on Architecture and Code Optimization"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2004.1268859"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"34","first-page":"197","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 (SAT '04"},{"key":"16","first-page":"1481","article-title":"A new clause learning scheme for efficient unsatisfiability proofs","author":"pipatsrisawat","year":"2008","journal-title":"AAAI Conference on Artificial Intelligence"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1504\/IJES.2005.008815"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2001.972816"},{"key":"14","article-title":"Results from the sat'04 sat solver competition","author":"le berre","year":"2004","journal-title":"7th International Conference on Theory and Applications of Satisfiability Testing"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2005.1466522"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"key":"38","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/11560548_10","article-title":"Automatic formal verification of liveness for pipelined processors with multicycle functional units","volume":"3725","author":"velev","year":"2005","journal-title":"13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '05"},{"journal-title":"IA-64 Application Developer's Architecture Guide","year":"1999","key":"12"},{"key":"21","first-page":"18","article-title":"Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking","author":"velev","year":"1998","journal-title":"Formal Methods in Computer-Aided Design (FMCAD '98) LNCS 1522"},{"key":"20","first-page":"24","volume":"20","author":"sharangpani","year":"2000","journal-title":"Itanium Processor Microarchitecture"},{"key":"43","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2011.5722201"},{"key":"42","first-page":"355","article-title":"Method for formal verification of soft-error tolerance mechanisms in pipelined microprocessors","volume":"6447","author":"velev","year":"2010","journal-title":"12th International Conference on Formal Engineering Methods (ICFEM '10"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2010.5419811"},{"key":"40","first-page":"8","article-title":"Exploiting hierarchical encodings of equality to design independent strategies in parallel smt decision procedures for a logic of equality 14th","author":"velev","year":"2009","journal-title":"Proc IEEE Int High Level Design Validation and Test Workshop (HLDVT)"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2011.6105403"},{"key":"44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24559-6_22"},{"key":"46","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2012.6165044"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309967"},{"key":"23","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","article-title":"Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic","volume":"1703","author":"velev","year":"1999","journal-title":"Correct Hardware Design and Verification Methods (CHARME '99"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337331"},{"key":"25","first-page":"296","article-title":"Formal verification of vliw microprocessors with speculative execution","author":"velev","year":"1855","journal-title":"Computer-Aided Verification (CAV '00"},{"key":"26","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"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998246"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(02)00091-3"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45206-5_16"},{"journal-title":"Solvable Cases of the Decision Problem","year":"1954","author":"ackermann","key":"3"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0087-0"},{"key":"10","article-title":"Bdd based procedures for a theory of equality with uninterpreted functions","volume":"1427","author":"goel","year":"1998","journal-title":"Computer-Aided Verification (CAV '98) LNCS"},{"key":"1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36126-X_8","article-title":"Relating multistep and single-step microprocessor correctness statements","volume":"2517","author":"aagaard","year":"2002","journal-title":"Formal Methods in Computer Aided Design (FMCAD 07)"},{"key":"30","first-page":"242","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":"Annals of Mathematics and Artificial Intelligence"},{"key":"7","article-title":"Automated verification of pipelined microprocessor control","author":"burch","year":"1994","journal-title":"Computer-Aided Verification (CAV '94) LNCS 818"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/566385.566390"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337588"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371364"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"4","doi-asserted-by":"crossref","DOI":"10.1109\/MSPEC.2009.5186555","article-title":"Cpu heal thyself: A fault-monitoring microprocessor design can save power or allow overclocking","author":"blaauw","year":"2009","journal-title":"IEEE Spectrum"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.2008.2007145"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240623"}],"event":{"name":"2014 15th International Symposium on Quality Electronic Design (ISQED)","start":{"date-parts":[[2014,3,3]]},"location":"Santa Clara, CA, USA","end":{"date-parts":[[2014,3,5]]}},"container-title":["Fifteenth International Symposium on Quality Electronic Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6779216\/6783285\/06783383.pdf?arnumber=6783383","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T12:14:45Z","timestamp":1565352885000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6783383\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":46,"URL":"https:\/\/doi.org\/10.1109\/isqed.2014.6783383","relation":{},"subject":[],"published":{"date-parts":[[2014,3]]}}}