{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:45:10Z","timestamp":1729676710245,"version":"3.28.0"},"reference-count":43,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1109\/memcod.2003.1210090","type":"proceedings-article","created":{"date-parts":[[2004,1,24]],"date-time":"2004-01-24T04:33:03Z","timestamp":1074918783000},"page":"65-74","source":"Crossref","is-referenced-by-count":12,"title":["Formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions"],"prefix":"10.1109","author":[{"given":"S.K.","family":"Srinivasan","sequence":"first","affiliation":[]},{"given":"M.N.","family":"Velev","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref39","DOI":"10.1007\/10722167_24"},{"doi-asserted-by":"publisher","key":"ref38","DOI":"10.1145\/337292.337331"},{"doi-asserted-by":"publisher","key":"ref33","DOI":"10.1109\/ASPDAC.1995.486361"},{"key":"ref32","article-title":"Formal Verification of an Avionics Microprocessor","author":"srivas","year":"1995","journal-title":"Technical Report CSL-95-04"},{"year":"0","journal-title":"Stanford Validity Checker (SVC)","key":"ref31"},{"doi-asserted-by":"publisher","key":"ref30","DOI":"10.1109\/40.877948"},{"key":"ref37","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 (CHARME '99"},{"key":"ref36","first-page":"113","article-title":"A Technique for Invariant Generation","volume":"2031","author":"tiwari","year":"2001","journal-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS'01)"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1023\/A:1008622002590","article-title":"A Practical Methodology for the Formal Verification of RISC Processors","volume":"13","author":"tahar","year":"1998","journal-title":"Formal Methods in System Design"},{"doi-asserted-by":"publisher","key":"ref34","DOI":"10.1007\/BFb0031822"},{"year":"0","journal-title":"EMBEDDED MIPS PROCESSOR CORE","key":"ref10"},{"key":"ref40","article-title":"Effective Use of Bool ean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors","author":"velev","year":"2001","journal-title":"38th Design Automation Conference (DAC'01)"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1109\/DATE.2002.998262"},{"year":"1993","author":"gordon","article-title":"Introduction to HOL: A Theorem Proving Environment for Higher OrderLogic","key":"ref12"},{"key":"ref13","article-title":"Systematic Verification of Pipelined Microprocessors","author":"hosabettu","year":"2000","journal-title":"Department of Computer Science"},{"key":"ref14","article-title":"Decomposing the Proof of Correctness of Pipelined Microprocessors","author":"hosabettu","year":"1998","journal-title":"Tenth Conference on Computer Aided Verification (CAV'98)"},{"doi-asserted-by":"publisher","key":"ref15","DOI":"10.1145\/296333.296345"},{"year":"0","journal-title":"Intel XScale Technology","key":"ref16"},{"year":"0","journal-title":"INTEGRITY RTOS","key":"ref17"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1007\/BFb0028750"},{"doi-asserted-by":"publisher","key":"ref19","DOI":"10.1109\/CMPASS.1996.507872"},{"year":"0","journal-title":"PC World","key":"ref28"},{"year":"0","journal-title":"ARM Technical Reference Manuals & Data Sheets","key":"ref4"},{"doi-asserted-by":"publisher","key":"ref27","DOI":"10.1109\/ICVD.1999.745161"},{"year":"0","journal-title":"allNetDevices","key":"ref3"},{"key":"ref6","first-page":"68","article-title":"Automated Verification of Pipelined Microprocessor Control","author":"burch","year":"1994","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref29","article-title":"Processor Verification with Precise Exceptions and Speculative Execution","author":"sawada","year":"1998","journal-title":"Computer-Aided Verification (CAV'98)"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1145\/240518.240623"},{"year":"0","journal-title":"Dell Axim X5","key":"ref8"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1109\/4.962279"},{"key":"ref2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36126-X_8","article-title":"Relating Multistep and Single-step Microprocessor Correctness Statements","author":"aagaard","year":"2002","journal-title":"Formal Methods in Computer Aided Design (FMCAD 07)"},{"doi-asserted-by":"publisher","key":"ref9","DOI":"10.1109\/LPE.1996.542723"},{"key":"ref1","article-title":"A Framework for Superscalar Microprocessor Correctness Statements","volume":"4","author":"aagaard","year":"2002","journal-title":"Software Tools for Technology Transfer"},{"key":"ref20","article-title":"Lockup-free Instruction Fetch\/Prefetch Cache Organization","author":"kroft","year":"1981","journal-title":"Proceedings of the International Symposium on Computer Architecture"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/500001.500053","article-title":"high-level automatic pipelining for sequential circuits","author":"marinescu","year":"2001","journal-title":"International Symposium on System Synthesis (IEEE Cat No 01EX526) ISSS-01"},{"doi-asserted-by":"publisher","key":"ref21","DOI":"10.1109\/HLDVT.2001.972816"},{"doi-asserted-by":"publisher","key":"ref42","DOI":"10.1016\/S0747-7171(02)00091-3"},{"year":"0","journal-title":"M•CORE microRISC Engine Programmer's Manual","key":"ref24"},{"key":"ref41","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44585-4_20","article-title":"EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations","author":"velev","year":"2001","journal-title":"Computer-Aided Verification (CAV ' 01)"},{"year":"2002","author":"marinescu","article-title":"Synthesis of Synchronous Pipelined Circuits from High-Level Modular Specifications","key":"ref23"},{"doi-asserted-by":"publisher","key":"ref26","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref43","article-title":"Integrating Formal Verification into an Advanced Computer Architecture Course","author":"velev","year":"2003","journal-title":"ASEE Annual Conference & Exposition"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1007\/978-0-387-35599-3_9"}],"event":{"name":"2003 1st IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2003)","start":{"date-parts":[[2003,6,24]]},"location":"Mont Saint Michel, France","end":{"date-parts":[[2003,6,26]]}},"container-title":["First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8593\/27232\/01210090.pdf?arnumber=1210090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T03:18:20Z","timestamp":1497583100000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210090\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":43,"URL":"https:\/\/doi.org\/10.1109\/memcod.2003.1210090","relation":{},"subject":[],"published":{"date-parts":[[2003]]}}}