Key points are not available for this paper at this time.
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’s 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.
Wang et al. (Sat,) studied this question.