{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:54Z","timestamp":1725551274594},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_4","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"23-36","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Explicitly Parallel Microprocessors"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"John","family":"Launchbury","sequence":"additional","affiliation":[]},{"given":"John","family":"Matthews","sequence":"additional","affiliation":[]},{"given":"Dick","family":"Kieburtz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"issue":"82","key":"4_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"2","author":"M. Abadi","year":"1991","unstructured":"Martin Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 2(82):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Allen, K. Kennedy, C. Porterfield, and J. Warren. Conversion of control dependence to data dependence. In The 10th ACM Symposium on Principles of Programming Languages, January 1983.","DOI":"10.1145\/567067.567085"},{"key":"4_CR3","unstructured":"David Bistry, Carole Delong, Mickey Gutman, Michael Julier, Michael Keith, Lawrence M. Mennemeir, Millind Mittal, Alex D. Peleg, and Uri Weiser. The Complete Guide to MMX Technology. McGraw-Hill, 1997."},{"key":"4_CR4","volume-title":"6th International Conference of Computer Aided Verification","author":"J. Burch","year":"1994","unstructured":"Jerry Burch and David Dill. Automatic verification of pipelined microprocessor control. In 6th International Conference of Computer Aided Verification, Stanford, California, June 1994."},{"key":"4_CR5","unstructured":"Brian Case. IA-64\u2019s static approach is controversial. Microprocessor Report, 11(16), 1997."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Werner Damm and Amir Pnueli. Verifying out-of-order executions.In Conference on Correct Hardware Design and Verification Methods,Montreal,Canada, 1997.","DOI":"10.1007\/978-0-387-35190-2_3"},{"key":"4_CR7","unstructured":"Keith Deifendorff. WinChip 4 thumbs nose at ILP. Microprocessor Report, 12(16), 1998."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Carole Delong. The IA-64 architecture at work. IEEE Computer, 31(7), 1998.","DOI":"10.1109\/2.689674"},{"key":"4_CR9","unstructured":"Kieth Diefendorff. Microarchitecture in the ditch. Microprocessor Report, 12(17), 1998."},{"key":"4_CR10","unstructured":"Linley Gwennap. Intel\u2019s P6 uses decoupled superscalar design. Microprocessor Report, 9(2), 1995."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Linley Gwennap. Digital 21264 sets new standard. itMicroprocessor Report, 14(10), 1996.","DOI":"10.7748\/ns.10.16.14.s24"},{"key":"4_CR12","unstructured":"Linley Gwennap. Intel, HP make EPIC disclosure. Microprocessor Report, 11(14), 1997."},{"key":"4_CR13","unstructured":"Linley Gwennap. AltiVec vectorizes PowerPC. Microprocessor Report, 12(6), 1998."},{"key":"4_CR14","unstructured":"Linley Gwennap. AMD deploys K6-2 with 3DNow. Microprocessor Report, 12 (7), 1998."},{"key":"4_CR15","unstructured":"Linley Gwennap. Intel outlines high-end roadmap. Microprocessor Report, 12(14), 1998."},{"key":"4_CR16","unstructured":"John L. Hennessy and David A. Patterson. Computer Architecture:A Quantitative Approach. Morgan Kaufmann, 1995."},{"key":"4_CR17","volume-title":"Formal Methods in Computer-Aided Design","author":"T. A. Henzinger","year":"1998","unstructured":"Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. An assume-guarantee rule for checking simulation. In Formal Methods in Computer-Aided Design, Palo Alto, California, 1998."},{"key":"4_CR18","volume-title":"Proceedings of the 22nd Annual International Symposium on Computer Architecture","author":"R. C. Ho","year":"1995","unstructured":"Richard C. Ho, C. Han Yang, Mark A. Horowitz, and David Dill. Architecture validation for processors. In Proceedings of the 22nd Annual International Symposium on Computer Architecture, Santa Margherita Ligure, Italy, 1995."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.","DOI":"10.1007\/BFb0028739"},{"key":"4_CR20","unstructured":"Dave Jaggar. Advanced RISC Machines Architectural Reference Manual. Prentice Hall, 1997."},{"key":"4_CR21","unstructured":"David Johnson. Techniques for mitigating memory latency in the the PA-8500 processor. In Hot Chips 10, Palo Alto, August 1998."},{"key":"4_CR22","unstructured":"Mike Johnson. Superscalar Microprocessor Design. Prentice Hall, 1991."},{"key":"4_CR23","unstructured":"Robert B. Jones, David L. Dill, and Jerry R. Burch. Efficient validity checking for processor verification. In Proceedings of the 1995 International Conference on Computer-Aided Design, San Jose, 1995."},{"key":"4_CR24","unstructured":"Vinod Kathail, Michael Schlansker, and B. Ramakrishna Rau. HPL PlayDoh architecture specification: Version 1.0. Technical Report HPL-93-80, Hewlett Packard Laboratories, 1993."},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison Wesley, 1997.","DOI":"10.1016\/S1353-4858(97)83033-4"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Ken McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.","DOI":"10.1007\/BFb0028738"},{"key":"4_CR27","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proceedings of 2nd International Joint Conference on Artificial Intelligence, The British Computer Society, 1971."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Zhenyu Qian. A formal specification of a large subset of Java virtual machine instructions for objects, methods and subroutines. In Formal Syntax and Semantics of Java. Springer-Verlog, 1998.","DOI":"10.1007\/3-540-48737-9_8"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"B. Ramakrishna Rau and Joseph A. Fisher. Instruction-level parallel processing: History, overview and perspective. The Journal of Supercomputing, 7(1), 1993.","DOI":"10.1007\/BF01205181"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Jun Sawada and Warren Hunt. Processor verification with precise exceptions and speculative execution.In International Conference on Computer-Aided Verification, Vancouver,Canada,July 1998.","DOI":"10.1007\/BFb0028740"},{"key":"4_CR31","unstructured":"Michael Schlansker, B.Ramakrishna Rau,, Scott Mahlke, Vinod Kathail, Richard Johnson, Sdum Anik,and Santosh G. Abraham. Achieving high levels of instruction-level parallelism with reduced hardware complexity.Technical Report HPL-96-120,Hewlett Packard Laboratories, 1996."},{"key":"4_CR32","unstructured":"Bruce Shriver and Bennett Smith. The Anatomy of a High-Performance Microprocessor: A Systems Perspective. IEEE Computer Society Press, 1998."},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Jens Skakkebaek, Robert Jones, and David Dill. Formal verification of out-of-order execution using incremental flushing. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.","DOI":"10.21236\/ADA400401"},{"key":"4_CR34","unstructured":"Peter Song. Demystifying EPIC and IA-64. Microprocessor Report, 12(1), 1998."},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"E.W. Stark. Ap roof technique for rely\/guarantee properties. In Proceedings of the 5th Conference on Foundations of Software Technology and Theoretical Computer Science, August 1985.","DOI":"10.1007\/3-540-16042-6_21"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Karen Stephenson. Towards an algebraic specification of the Java virtual machine. In Prospects for Hardware Foundations. Springer-Verlog, 1998.","DOI":"10.1007\/3-540-49254-2_7"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Dean M. Tullsen, Susan J. Eggers, Joel S. Emer, Henry M. Levy, Jack L. Lo, and Rebecca L. Stamm. Exploiting choice: Instruction fetch and issue on an implementable simultaneous multithreading processor. In 23rd Annual International Symposium on Computer Architecture, Philadelphia, PA, May 1996.","DOI":"10.1145\/232973.232993"},{"key":"4_CR38","unstructured":"Miroslav N. Velev and Randal E. Bryant. Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. In FormalMethods in Computer-Aided Design, Palo Alto, California, 1998."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:10:04Z","timestamp":1558278604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"3 June 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}