{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T13:13:05Z","timestamp":1753881185467,"version":"3.41.2"},"reference-count":19,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2010,9,8]],"date-time":"2010-09-08T00:00:00Z","timestamp":1283904000000},"content-version":"vor","delay-in-days":250,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Journal of Electrical and Computer Engineering"],"published-print":{"date-parts":[[2010,1]]},"abstract":"<jats:p>We develop two optimization techniques,<jats:italic>flush-machine<\/jats:italic>and collapsed flushing, to improve the efficiency of automatic refinement\u2010abased verification of out\u2010of\u2010order (ooo) processor models. Refinement is a notion of equivalence that can be used to check that an ooo processor correctly implements all behaviors of its instruction set architecture (ISA), including deadlock detection. The optimization techniques work by reducing the computational complexity of the refinement map, a function central to refinement proofs that maps ooo processor model states to ISA states. This has a direct impact on the efficiency of verification, which is studied using 23 ooo processor models.<jats:italic>Flush-machine<\/jats:italic>, is a novel optimization technique. Collapsed flushing has been employed previously in the context of in\u2010order processors. We show how to apply collapsed flushing for ooo processor models. Using both the optimizations together, we can handle 9 ooo models that could not be verified using standard flushing. Also, the optimizations provided a speed up of 23.29 over standard flushing.<\/jats:p>","DOI":"10.1155\/2010\/515021","type":"journal-article","created":{"date-parts":[[2010,9,8]],"date-time":"2010-09-08T18:35:03Z","timestamp":1283970903000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Optimization Techniques for Verification of Out\u2010of\u2010Order Execution Machines"],"prefix":"10.1155","volume":"2010","author":[{"given":"Sudarshan K.","family":"Srinivasan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,9,8]]},"reference":[{"key":"e_1_2_8_1_2","doi-asserted-by":"crossref","unstructured":"YanyanG.andXiL. Formal verification of out-of-order processor Proceedings of the International Conference on Computer Modeling and Simulation (ICCMS \u203209) February 2009 IEEE 129\u2013135 2-s2.0-64849097034 https:\/\/doi.org\/10.1109\/ICCMS.2009.47.","DOI":"10.1109\/ICCMS.2009.47"},{"key":"e_1_2_8_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/40.768503"},{"key":"e_1_2_8_3_2","doi-asserted-by":"crossref","unstructured":"HosabettuR. SrivasM. andGopalakrishnanG. HalbwachsN.andPeledD. Proof of correctness of a processor with reorder buffer using the completion functions approach 1633 Proceedings of the International Conference on Computer Aided Verification (CAV \u203299) 1999 Springer Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-48683-6_7"},{"key":"e_1_2_8_4_2","doi-asserted-by":"crossref","unstructured":"AronsT.andPnueliA. A comparison of two verification methods for speculative instruction execution 1785 Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u203200) March 2000 Springer 487\u2013502 Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-46419-0_33"},{"key":"e_1_2_8_5_2","unstructured":"KroningD. Formal verification of pipelined microprocessors Ph.D. thesis 2001 Universit\u00e4t des Saarlandes."},{"key":"e_1_2_8_6_2","doi-asserted-by":"crossref","unstructured":"LahiriS. SeshiaS. andBryantR. Modeling and verification of out-of-order microprocessors using UCLID 2517 Proceedings of the Formal Methods in Computer-Aided Design (FMCAD \u203202) 2002 Springer 142\u2013159 Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-36126-X_9"},{"key":"e_1_2_8_7_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014118529369"},{"key":"e_1_2_8_8_2","doi-asserted-by":"crossref","unstructured":"VelevM. N. Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer Proceedings of the Design Automation and Test in Europe (DATE \u203202) 2002 IEEE Computer Society 28\u201335.","DOI":"10.1109\/DATE.2002.998246"},{"key":"e_1_2_8_9_2","doi-asserted-by":"crossref","unstructured":"ShehataH. I.andAagaardM. MalikS. FixL. andKahngA. B. A general decomposition strategy for verifying register renaming Proceedings of the Design Automation Conference (DAC \u203204) 2004 ACM 234\u2013237.","DOI":"10.1145\/996566.996632"},{"key":"e_1_2_8_10_2","unstructured":"VelevM. N. Using automatic case splits and efficient cnf translation to guide a sat-solver when formally verifying out-of-order processors Proceedings of the AMAI Symposium 2004."},{"key":"e_1_2_8_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.18"},{"key":"e_1_2_8_12_2","article-title":"DIVA: a dynamic approach to microprocessor verification","volume":"2","author":"Austin T. M.","year":"2000","journal-title":"Journal of Instruction-Level Parallelism"},{"key":"e_1_2_8_13_2","doi-asserted-by":"crossref","unstructured":"BentleyB. Validating the Intel Pentium 4 microprocessor Proceedings of the 38th Design Automation Conference June 2001 244\u2013248 2-s2.0-0034840742.","DOI":"10.1145\/378239.378473"},{"key":"e_1_2_8_14_2","unstructured":"ManoliosP. Mechanical verification of reactive systems Ph.D. thesis August2001 University of Texas Austin Tex USA http:\/\/www.ccs.neu.edu\/home\/pete\/research\/phd\u2010dissertation.html."},{"key":"e_1_2_8_15_2","doi-asserted-by":"crossref","unstructured":"BurchJ. R.andDillD. L. Automatic verification of pipelined microprocessor control 818 Proceedings of the International Conference on Computer Aided Verification (CAV \u203294) 1994 Springer 68\u201380 Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"e_1_2_8_16_2","unstructured":"ManoliosP. HuntW. A.Jr.andJohnsonS. D. Correctness of pipelined machines 1954 Proceedings of the Formal Methods in Computer-Aided Design (FMCAD \u203200) 2000 Springer 161\u2013178 Lecture Notes in Computer Science."},{"key":"e_1_2_8_17_2","doi-asserted-by":"crossref","unstructured":"KaneR. ManoliosP. andSrinivasanS. K. GielenG. G. E. Monolithic verification of deep pipelines with collapsed flushing Proceedings of the Design Automation and Test in Europe (DATE \u203206) 2006 Leuven Belgium European Design and Automation Association 1234\u20131239.","DOI":"10.1109\/DATE.2006.244077"},{"key":"e_1_2_8_18_2","doi-asserted-by":"crossref","unstructured":"VelevM. N.andBryantR. E. Formal verification of superscalar microprocessors with multicycle functional units exceptions and branch prediction Proceedings of the 37th Design Automation Conference (DAC \u203200) June 2000 112\u2013117 2-s2.0-0033684177.","DOI":"10.1145\/337292.337331"},{"key":"e_1_2_8_19_2","doi-asserted-by":"crossref","unstructured":"VelevM. N. mvelev@ece.emu.edu BorrioneD.andPaulW. J. Automatic formal verification of liveness for pipelined processors with multicycle functional units 3725 Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME \u203205) 2005 Springer 97\u2013113 Lecture Notes in Computer Science 2-s2.0-0037331793 https:\/\/doi.org\/10.1007\/11560548_10.","DOI":"10.1007\/11560548_10"}],"container-title":["Journal of Electrical and Computer Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jece\/2010\/515021.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jece\/2010\/515021.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1155\/2010\/515021","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T17:08:09Z","timestamp":1740503289000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1155\/2010\/515021"}},"subtitle":[],"editor":[{"given":"Dhiraj K.","family":"Pradhan","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["10.1155\/2010\/515021"],"URL":"https:\/\/doi.org\/10.1155\/2010\/515021","archive":["Portico"],"relation":{},"ISSN":["2090-0147","2090-0155"],"issn-type":[{"type":"print","value":"2090-0147"},{"type":"electronic","value":"2090-0155"}],"subject":[],"published":{"date-parts":[[2010,1]]},"assertion":[{"value":"2010-03-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-08-17","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"515021"}}