{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:36:34Z","timestamp":1742391394795},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_9","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:55:19Z","timestamp":1269885319000},"page":"142-159","source":"Crossref","is-referenced-by-count":43,"title":["Modeling and Verification of Out-of-Order Microprocessors in UCLID"],"prefix":"10.1007","author":[{"given":"Shuvendu K.","family":"Lahiri","sequence":"first","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"T. Arons and A. Pnueli. Verifying Tomasulo\u2019s algorithm by Refinement. In Proc. VLSI Design Conference (VLSI\u2019 99), 1999.","DOI":"10.1109\/ICVD.1999.745165"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"T. Arons and A. Pnueli. A comparison of two verification methods for speculative instruction execution. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), March 2000.","DOI":"10.1007\/3-540-46419-0_33"},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u2019 96)","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 96), LNCS 1166, pages 187\u2013201. Springer-Verlag, November 1996."},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49519-3_24","volume-title":"Formal Methods in Computer-Aided Design(FMCAD\u2019 98)","author":"S. Berezin","year":"1998","unstructured":"S. Berezin, A. Biere, E. M. Clarke, and Y. Zhu. Combining symbolic model checking with uninterpreted functions for out of order microprocessor verification. In Formal Methods in Computer-Aided Design(FMCAD\u2019 98), LNCS 1522. Springer-Verlag, November 1998."},{"key":"9_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer-Aided Verification (CAV\u2019 99)","author":"R. E. Bryant","year":"1999","unstructured":"R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification (CAV\u2019 99), LNCS 1633, pages 470\u2013482. Springer-Verlag, July 1999."},{"issue":"1","key":"9_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/371282.371364","volume":"2","author":"R. E. Bryant","year":"2001","unstructured":"R. E. Bryant, S. German, and M. N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic, 2(1):1\u201341, January 2001.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proc. Computer-Aided Verification (CAV\u201902) (to appear), July 2002.","DOI":"10.1007\/3-540-45657-0_7"},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer-Aided Verification (CAV\u2019 94)","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automated verification of pipelined microprocessor control. In D. L. Dill, editor, Computer-Aided Verification (CAV\u2019 94), LNCS 818, pages 68\u201380. Springer-Verlag, June 1994."},{"issue":"2","key":"9_CR9","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1017\/S0022481200051513","volume":"41","author":"Y. Gurevich","year":"1976","unstructured":"Y. Gurevich. The decision problem for standard classes. The Journal of Symbolic Logic, 41(2):460\u2013464, June 1976.","journal-title":"The Journal of Symbolic Logic"},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_7","volume-title":"Computer-Aided Verification (CAV 1999)","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, G. Gopalakrishnan, and M. Srivas. Proof of correctness of a processor with reorder buffer using the completion function approach. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification (CAV 1999), volume 1633 of Lecture Notes in Computer Science. Springer-Verlag, July 1999."},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_39","volume-title":"Computer-Aided Verification (CAV 2000)","author":"R. Hosabettu","year":"2000","unstructured":"R. Hosabettu, G. Gopalakrishnan, and M. Srivas. Verifying advanced microarchitectures that support speculation and exceptions. In A. Emerson and P. Sistla, editors, Computer-Aided Verification (CAV 2000), LNCS 1855. Springer-Verlag, July 2000."},{"key":"9_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer-Aided Verification","author":"R. Jhala","year":"2001","unstructured":"R. Jhala and K. McMillan. Microarchitecture verification by compositional model checking. In G. Berry, H. Comon, and A. Finkel, editors, Computer-Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 396\u2013410. Springer-Verlag, July 2001."},{"key":"9_CR13","unstructured":"S. Lahiri, C. Pixley, and K. Albin. Experience with term level modeling and verification of the MCORE microprocessor core. In Proc. IEEE High Level Design Validation and Test (HLDVT 2001), November 2001."},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738","volume-title":"Computer-Aided Verification (CAV 1998)","author":"K. McMillan","year":"1998","unstructured":"K. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Computer-Aided Verification (CAV 1998), volume 1427 of Lecture Notes in Computer Science Springer-Verlag, June 1998."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In 38th Design Automation Conference (DAC\u2019 01), June 2001.","DOI":"10.1145\/378239.379017"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752. Springer-Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028740","volume-title":"Computer-Aided Verification (CAV\u2019 98)","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. Hunt. Processor verification with precise exceptions and speculative execution. In A. J. Hu and M. Y. Vardi, editors, Computer-Aided Verification (CAV\u2019 98), LNCS 1427. Springer-Verlag, June 1998."},{"key":"9_CR18","unstructured":"J. P. Shen and M. Lipasti. Fundamentals of Superscalar Processor Design. In Press, 2001."},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification (CAV\u2019 98)","author":"J. U. Skakkaebaek","year":"1998","unstructured":"J. U. Skakkaebaek, R. B. Jones, and D. L. Dill. Formal verification of out-of-order execution using incremental flushing. In A. J. Hu and M. Y. Vardi, editors, Computer-Aided Verification (CAV\u2019 98), LNCS 1427. Springer-Verlag, June 1998."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"M. N. Velev. Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer. In Design, Automation and Test in Europe (DATE\u2019 02), pages 28\u201335, March 2002.","DOI":"10.1109\/DATE.2002.998246"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"M. N. Velev and R. E. Bryant. Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions and Branch Predication. In 37th Design Automation Conference (DAC\u2019 00), June 2000.","DOI":"10.1145\/337292.337331"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:27:00Z","timestamp":1558970820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}