{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:13Z","timestamp":1740028753814,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-48153-2_5","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"37-53","source":"Crossref","is-referenced-by-count":16,"title":["Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic"],"prefix":"10.1007","author":[{"given":"Miroslav N.","family":"Velev","sequence":"first","affiliation":[]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"5_CR1","unstructured":"W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954."},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"R.E. Bryant, \u201cSymbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,\u201d ACM Computing Serveys, Vol. 24, No. 3 (September 1992), pp. 293\u2013318.","journal-title":"ACM Computing Serveys"},{"key":"5_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification (CAV\u201999)","author":"R.E. Bryant","year":"1999","unstructured":"R.E. Bryant, S. German, and M.N. Velev, \u201cExploiting Positive Equality in a Logic of Equality with Uninterpreted Functions, \u201c2 Computer-Aided Verification (CAV\u201999), LNCS, Springer-Verlag, June 1999."},{"key":"5_CR4","unstructured":"R.E. Bryant, S. German, and M.N. Velev, \u201cProcessor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,\u201d2 Technical Report CMU-CS-99-115, Carnegie Mellon University, 1999."},{"key":"5_CR5","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\u201894)","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, and D.L. Dill, \u201cAutomated Verification of Pipelined Microprocessor Control,\u201d Computer-Aided Verification (CAV\u201894), D.L. Dill, ed., LNCS 818, Springer-Verlag, June 1994, pp. 68\u201380. Available from: http:\/\/sprout.stanford.edu\/papers.html ."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"J.R. Burch, \u201cTechniques for Verifying Superscalar Microprocessors,\u201d 33rd Design Automation Conference (DAC\u201996), June 1996, pp. 552\u2013557.","DOI":"10.1145\/240518.240623"},{"key":"5_CR7","unstructured":"CUDD-2.3.0,URL: http:\/\/vlsi.colorado.edu\/~fabio ."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Computer-Aided Verification (CAV\u201998)","author":"A. Goel","year":"1998","unstructured":"A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal, \u201cBDD Based Procedures for a Theory of Equality with Uninterpreted Functions, \u201dComputer-Aided Verification (CAV\u201998), A.J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June 1998, pp. 244\u2013255."},{"key":"5_CR9","unstructured":"GRASP,URL: http:\/\/andante.eecs.umich.edu ."},{"key":"5_CR10","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"1996","unstructured":"J.L. Hennessy, and D.A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996.","edition":"2nd edition"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare, \u201cProof of Correctness of Data Representations,\u201d Acta Informatica, 1972, Vol. 1, pp. 271\u2013281.","journal-title":"Acta Informatica"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"R. Hojati, A. Kuehlmann, S. German, and R.K. Brayton, \u201cValidity Checking in the Theory of Equality with Uninterpreted Functions Using Finite Instantiations,\u201c International Workshop on Logic Synthesis, May 1997.","DOI":"10.1007\/BFb0031810"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/BFb0028750","volume-title":"Computer-Aided Verification (CAV\u201898)","author":"A.J. Isles","year":"1998","unstructured":"A.J. Isles, R. Hojati, and R.K. Brayton, \u201cComputing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory, \u201dComputer-Aided Verification (CAV\u201898), A.J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June 1998, pp. 256\u2013267."},{"issue":"5","key":"5_CR14","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"J.P. Marques-Silva, and K.A. Sakallah, \u201cGRASP: A Search Algorithm for Propositional Satisfiability, \u201d IEEE Transactions on Computers, Vol. 48, No. 5, May 1999, pp. 506\u2013521.","journal-title":"IEEE Transactions on Computers"},{"key":"5_CR15","series-title":"Lect Notes Comput Sci","first-page":"1999","volume-title":"Computer-Aided Verification (CAV\u201999)","author":"A. Pnueli","year":"1999","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel, \u201cDeciding Equality Formulas by Small-Domain Instantiations\u201d, Computer-Aided Verification (CAV\u201999), LNCS, Springer-Verlag, June 1999."},{"key":"5_CR16","unstructured":"G. St\u00e5lmarck, \u201cA System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula\u201d, Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995), 1989."},{"key":"5_CR17","unstructured":"Stanford Validity Checker (SVC), URL: http:\/\/sprout.Stanford.EDU\/SVC ."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"M.N. Velev, and R.E. Bryant, \u201cVerification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation,\u201d2 International Conference on Application of Concurrency to System Design (CSD\u201898), IEEE Computer Society, March 1998, pp. 200\u2013212.","DOI":"10.1109\/CSD.1998.657552"},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-49519-3_3","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u201998)","author":"M.N. Velev","year":"1998","unstructured":"M.N. Velev, and R.E. Bryant, \u201cBit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking,\u201d2 Formal Methods in Computer-Aided Design (FMCAD\u201998), G. Gopalakrishnan and P. Windley, eds., LNCS 1522, Springer-Verlag, November 1998, pp. 18\u201335."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"M.N. Velev, and R.E. Bryant, \u201cExploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors,\u201d2 36th Design Automaation Conference (DAC\u201999), June 1999, pp. 397\u2013401.","DOI":"10.1145\/309847.309967"},{"key":"5_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/BFb0031821","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u201996)","author":"P.J. Windley","year":"1996","unstructured":"P.J. Windley, and J.R. Burch, \u201cMechanically Checking a Lemma Used in an Automatic Verification Tool, \u201d Formal Methods in Computer-Aided Design (FMCAD\u201996), M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. 362\u2013376."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"H. Zhang, \u201cSATO: An Efficient Propositional Prover,\u201d International Conference on Automated Deduction (CADE\u201997), LNAI 1249, Springer-Verlag, 1997, pp. 272\u2013275. Available from: http:\/\/www.cs.uiowa.edu\/~hzhang\/sato.html .","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:16:02Z","timestamp":1739992562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540665595","9783540481539"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1997]]}}}