{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:49:33Z","timestamp":1783684173735,"version":"3.55.0"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,6]]},"DOI":"10.1109\/memcod.2008.4547694","type":"proceedings-article","created":{"date-parts":[[2008,6,20]],"date-time":"2008-06-20T11:40:32Z","timestamp":1213962032000},"page":"89-100","source":"Crossref","is-referenced-by-count":3,"title":["Directed-Logical Testing for Functional Verification of Microprocessors"],"prefix":"10.1109","author":[{"given":"Michael","family":"Katelman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","author":"patterson","year":"1990","journal-title":"Computer Architecture A Quantitative Approach"},{"key":"17","year":"0"},{"key":"18","author":"mishra","year":"2004"},{"key":"15","article-title":"the temporal logic of rewriting","author":"meseguer","year":"2007"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1127908.1127991"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.06.007"},{"key":"12","first-page":"1240","article-title":"functional test generation using property decompositions for validation of pipelined processors","author":"koo","year":"2006","journal-title":"Proc DATE Design Automation and Test in Europe"},{"key":"21","first-page":"3","article-title":"a case study in formal verification of register-transfer logic with acl2: the floating point adder of the amd athlon processor","volume":"1954","author":"russinoff","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.850814"},{"key":"23","first-page":"175","article-title":"micro architecture coverage directed generation of test programs","author":"ur","year":"1999","journal-title":"Proc Design Automation Conf DAC"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065788"},{"key":"25","year":"0"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2004.1277900"},{"key":"2","year":"0"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.833614"},{"key":"1","year":"0"},{"key":"7","author":"clavel","year":"2007","journal-title":"All About Maude - A High-Performance Logical Framework"},{"key":"6","first-page":"185","article-title":"high-level test generation for design verification of pipelined microprocessors","author":"campenhout","year":"1999","journal-title":"Proc Design Automation Conf DAC"},{"key":"5","first-page":"68","article-title":"automatic verification of pipelined microprocessor control","volume":"818","author":"burch","year":"1994","journal-title":"Springer LNCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/11799573_9"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.03.017"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.049"}],"event":{"name":"2008 6th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE '08)","location":"Anaheim, CA, USA","start":{"date-parts":[[2008,6,5]]},"end":{"date-parts":[[2008,6,7]]}},"container-title":["2008 6th ACM\/IEEE International Conference on Formal Methods and Models for Co-Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4542603\/4547672\/04547694.pdf?arnumber=4547694","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,16]],"date-time":"2017-03-16T19:09:59Z","timestamp":1489691399000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4547694\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/memcod.2008.4547694","relation":{},"subject":[],"published":{"date-parts":[[2008,6]]}}}