{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T02:28:18Z","timestamp":1747189698275,"version":"3.40.5"},"reference-count":18,"publisher":"World Scientific Pub Co Pte Ltd","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:p> This paper introduces an innovative translation validation framework designed for MLIR-based compilers, which has garnered considerable prominence in fields such as machine learning, high-performance computing and hardware design. Despite rigorous testing, compilers based on MLIR might still induce incorrect results and undefined behaviors, necessitating verification work. Our framework first takes a pair of MLIR programs as inputs and check their function signature\u2019s compatibility before encoding them into SMT expressions. Then it uses the Z3 SMT solver to check whether the target program refines the source program. Our framework transcends the dialect limitations of past solutions, thereby providing validation support to a wider range of MLIR-based compilers. We demonstrate its effectiveness through evaluations on prominent open-source MLIR-based compilers, where we identified bugs and undefined behaviors. We further demonstrate the capability of this framework by validating two practical deep-learning accelerator designs. <\/jats:p>","DOI":"10.1142\/s021819402450030x","type":"journal-article","created":{"date-parts":[[2024,6,8]],"date-time":"2024-06-08T04:50:40Z","timestamp":1717822240000},"page":"1621-1640","source":"Crossref","is-referenced-by-count":0,"title":["A Systematic Translation Validation Framework for MLIR-Based Compilers"],"prefix":"10.1142","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1314-2262","authenticated-orcid":false,"given":"Yanzhao","family":"Wang","sequence":"first","affiliation":[{"name":"Portland State University, Portland, OR 97201, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7324-3287","authenticated-orcid":false,"given":"Fei","family":"Xie","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, OR 97201, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7567-2870","authenticated-orcid":false,"given":"Zhenkun","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation, Hillsboro, OR 97124, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1038-3482","authenticated-orcid":false,"given":"Pasquale","family":"Cocchini","sequence":"additional","affiliation":[{"name":"Intel Corporation, Hillsboro, OR 97124, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4372-926X","authenticated-orcid":false,"given":"Jin","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation, Hillsboro, OR 97124, USA"}]}],"member":"219","published-online":{"date-parts":[[2024,7,19]]},"reference":[{"key":"S021819402450030XBIB001","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"S021819402450030XBIB002","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"S021819402450030XBIB003","first-page":"12","volume-title":"IMPACT","author":"Moses W. S.","year":"2021"},{"key":"S021819402450030XBIB006","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293910"},{"key":"S021819402450030XBIB007","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA53966.2022.00060"},{"key":"S021819402450030XBIB008","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"S021819402450030XBIB009","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_19"},{"key":"S021819402450030XBIB010","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"S021819402450030XBIB011","doi-asserted-by":"publisher","DOI":"10.1145\/3528416.3530866"},{"volume-title":"Workshop on Open-Source EDA Technology (WOSET)","year":"2021","author":"Eldridge S.","key":"S021819402450030XBIB013"},{"key":"S021819402450030XBIB014","first-page":"1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th Eur. Congress","author":"Leroy X.","year":"2016"},{"key":"S021819402450030XBIB015","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"S021819402450030XBIB016","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"S021819402450030XBIB017","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00120"},{"key":"S021819402450030XBIB018","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3605239"},{"key":"S021819402450030XBIB019","first-page":"1","volume-title":"Proc. 2024 ACM SIGPLAN Symp. Principles of Programming Languages (POPL)","author":"Zhao J.","year":"2024"},{"key":"S021819402450030XBIB020","first-page":"209","volume-title":"OSDI\u201908: Proc. 8th USENIX Conf. Operating Systems Design and Implementation","author":"Cadar C.","year":"2008"},{"key":"S021819402450030XBIB022","doi-asserted-by":"publisher","DOI":"10.1145\/3028687.3041020"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S021819402450030X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T08:59:08Z","timestamp":1729155548000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S021819402450030X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,19]]},"references-count":18,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["10.1142\/S021819402450030X"],"URL":"https:\/\/doi.org\/10.1142\/s021819402450030x","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"type":"print","value":"0218-1940"},{"type":"electronic","value":"1793-6403"}],"subject":[],"published":{"date-parts":[[2024,7,19]]}}}