{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:36:39Z","timestamp":1750307799766,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-0429924IS-0417413CCF-043887EPS-0447679"],"award-info":[{"award-number":["CCF-0429924IS-0417413CCF-043887EPS-0447679"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005714","name":"Office of Experimental Program to Stimulate Competitive Research","doi-asserted-by":"publisher","award":["CCF-0429924IS-0417413CCF-043887EPS-0447679"],"award-info":[{"award-number":["CCF-0429924IS-0417413CCF-043887EPS-0447679"]}],"id":[{"id":"10.13039\/100005714","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:p>We show how to automatically verify that complex pipelined machine models satisfy the same safety and liveness properties as their instruction-set architecture (ISA) models by using well-founded equivalence bisimulation (WEB) refinement. We show how to reduce WEB-refinement proof obligations to formulas expressible in the decidable logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). This allows us to automate the verification of the pipelined machine models by using the UCLID decision procedure to transform CLU formulas to Boolean satisfiability problems. To relate pipelined machine states to ISA states, we use the commitment and flushing refinement maps. We evaluate our work using 17 pipelined machine models that contain various features, including deep pipelines, precise exceptions, branch prediction, interrupts, and instruction queues. Our experimental results show that the overhead of proving liveness, obtained by comparing the cost of proving both safety and liveness with the cost of only proving safety, is about 17%, but depends on the refinement map used; for example, the liveness overhead is 23% when flushing is used and is negligible when commitment is used.<\/jats:p>","DOI":"10.1145\/1367045.1367054","type":"journal-article","created":{"date-parts":[[2008,7,29]],"date-time":"2008-07-29T13:22:19Z","timestamp":1217337739000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Automatic verification of safety and liveness for pipelined machines using WEB refinement"],"prefix":"10.1145","volume":"13","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, MA"}]},{"given":"Sudarshan K.","family":"Srinivasan","sequence":"additional","affiliation":[{"name":"North Dakota State University, Fargo, ND"}]}],"member":"320","published-online":{"date-parts":[[2008,7,25]]},"reference":[{"volume":"2144","volume-title":"Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)","author":"Aagaard M.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0087-0"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022917321255"},{"volume":"1785","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Arons T.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378473"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_2"},{"volume":"1633","volume-title":"Proceedings of the Computer-Aided Verification (CAV)","author":"Bryant R. E.","key":"e_1_2_1_7_1"},{"volume":"2404","volume-title":"Proceedings of the Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, eds. Lecture Notes in Computer Science","author":"Bryant R. E.","key":"e_1_2_1_8_1"},{"volume":"818","volume-title":"Proceedings of the Computer-Aided Verification (CAV), D. L. Dill, ed. Lecture Notes in Computer Science","author":"Burch J. R.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","unstructured":"de Moura L. 2006. Yices homepage. http:\/\/fm.csl.sri.com\/yices.]]  de Moura L. 2006. Yices homepage. http:\/\/fm.csl.sri.com\/yices.]]"},{"volume":"3114","volume-title":"Proceedings of the Computer-Aided Verification (CAV)","author":"Ganzinger H.","key":"e_1_2_1_11_1"},{"volume":"1633","volume-title":"Proceedings of the Computer-Aided Verification (CAV)","author":"Hosabettu R.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/296333.296345"},{"volume":"1522","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD)","author":"Jones R.","key":"e_1_2_1_14_1"},{"volume-title":"Proceedings of the Design Automation and Test in Europe (DATE)","author":"Kane R.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Kaufmann M. Manolios P. and Moore J. S. Eds. 2000a. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic.]]   Kaufmann M. Manolios P. and Moore J. S. Eds. 2000a. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic.]]","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Kaufmann M. Manolios P. and Moore J. S. 2000b. Computer-Aided Reasoning: An Approach. Kluwer Academic.]]   Kaufmann M. Manolios P. and Moore J. S. 2000b. Computer-Aided Reasoning: An Approach. Kluwer Academic.]]","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_2_1_18_1","unstructured":"Kroening D. 2001. Formal verification of pipelined microprocessors. Ph.D. thesis Universit\u00e4t des Saarlandes.]]  Kroening D. 2001. Formal verification of pipelined microprocessors. Ph.D. thesis Universit\u00e4t des Saarlandes.]]"},{"volume":"2517","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD)","author":"Lahiri S.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.461.0053"},{"volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD), W. A. H., Jr","author":"Manolios P.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","unstructured":"Manolios P. 2001. Mechanical verification of reactive systems. Ph.D. thesis University of Texas at Austin. http:\/\/www.cc.gatech.edu\/~manolios\/publications.html.]]  Manolios P. 2001. Mechanical verification of reactive systems. Ph.D. thesis University of Texas at Austin. http:\/\/www.cc.gatech.edu\/~manolios\/publications.html.]]"},{"volume-title":"Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME)","author":"Manolios P.","key":"e_1_2_1_23_1"},{"volume-title":"Tech. Rep. GIT-CERCS-03-17","year":"2003","author":"Manolios P.","key":"e_1_2_1_24_1"},{"volume-title":"Proceedings of the Design, Automation, and Test in Europe (DATE). IEEE Computer Society, 168--175","author":"Manolios P.","key":"e_1_2_1_25_1"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD)","author":"Manolios P.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487914"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Manolios P. and Srinivasan S. K. 2005c. A parameterized benchmark suite of hard pipelined machine verification problems. http:\/\/www.cc.gatech.edu\/~manolios\/benchmarks\/charme.html.]]  Manolios P. and Srinivasan S. K. 2005c. A parameterized benchmark suite of hard pipelined machine verification problems. http:\/\/www.cc.gatech.edu\/~manolios\/benchmarks\/charme.html.]]","DOI":"10.1007\/11560548_32"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.257"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733764"},{"volume":"219","volume-title":"Proceedings of the IFIP WCC Stream 7 on Distributed and Parallel Embedded Systems (DIPES)","author":"Mishra P.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","unstructured":"Owre S. Shankar N. Rushby J. M. and Stringer-Calvert D. W. J. 2001. PVS system guide. http:\/\/pvs.csl.sri.com\/doc\/pvs-system-guide.pdf.]]  Owre S. Shankar N. Rushby J. M. and Stringer-Calvert D. W. J. 2001. PVS system guide. http:\/\/pvs.csl.sri.com\/doc\/pvs-system-guide.pdf.]]"},{"volume-title":"Proceedings of the 12th International Conference on VLSI Design","author":"Patankar V. A.","key":"e_1_2_1_33_1"},{"key":"e_1_2_1_34_1","unstructured":"Ryan L. 2008. Siege homepage. http:\/\/www.cs.sfu.ca\/~loryan\/personal.]]  Ryan L. 2008. Siege homepage. http:\/\/www.cs.sfu.ca\/~loryan\/personal.]]"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Sawada J. 1999. Formal verification of an advanced pipelined machine. Ph.D. thesis University of Texas at Austin. http:\/\/www.cs.utexas.edu\/users\/sawada\/dissertation\/.]]   Sawada J. 1999. Formal verification of an advanced pipelined machine. Ph.D. thesis University of Texas at Austin. http:\/\/www.cs.utexas.edu\/users\/sawada\/dissertation\/.]]","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014122630277"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.57892"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1015090.1015165"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337331"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1367045.1367054","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1367045.1367054","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:30Z","timestamp":1750254990000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1367045.1367054"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1145\/1367045.1367054"],"URL":"https:\/\/doi.org\/10.1145\/1367045.1367054","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2008,7]]},"assertion":[{"value":"2005-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}