MLIR-TV is an SMT-based translation validation framework for MLIR. This project is inspired by Alive2, an SMT-based bounded translation validation framework for LLVM IR. MLIR-TV focuses on supporting dialects that are tailored for compiling machine learning applications.
Prerequisites: CMake(>=3.13),
MLIR,
Python3,
Solvers (at least one of them must be used):
z3-4.8.13 ,
cvc5-0.0.3(limited support)
Optional prerequisites: Ninja
You will need to build & install MLIR.
Please follow LLVM's Getting Started, and run cmake --build . --target install.
If you already have your MLIR built but found that you are not sudo priviledge that is to install, you can update the CMAKE_INSTALL_PREFIX variable via
cmake -DCMAKE_INSTALL_PREFIX=<your local path> ../llvm and run the install command.
You will also need to build & install Z3.
Please build Z3 using CMake and install it to somewhere designated by CMAKE_INSTALL_PREFIX.
cmake -Bbuild \
# We recommend you use Ninja if you have it on your system
[-GNinja] \
# At least one of USE_Z3 and USE_cvc5 should be set to ON. Build will fail otherwise.
[-DUSE_Z3=ON|OFF] \
[-DUSE_cvc5=ON|OFF] \
# Use <dep>_ROOT variables when CMake fails to locate dependencies on its own
[-DMLIR_ROOT=/mlir/installation/path] \
[-DZ3_ROOT=/z3/installation/path] \
[-Dcvc5_ROOT=/cvc5/installation/path] \
# Set -USE_LIBC to ON iff the MLIR (and cvc5) is linked with libc++
[-DUSE_LIBC=ON|OFF] \
[-DCMAKE_BUILD_TYPE=Debug|Release]
# You may omit -j if you're using Ninja
cmake --build build --target mlir-tv -jMLIR-TV takes two .mlir files that contain MLIR functions of identical signatures.
Run the built mlir-tv executable as following:
mlir-tv <.mlir before opt> <.mlir after opt>
# ex: ./build/mlir-tv \
# tests/opts/conv2d-to-img2col/nhwc_filter.src.mlir \
# tests/opts/conv2d-to-img2col/nhwc_filter.tgt.mlir -smt-to=5000cd build
# A detailed log will be written to build/Testing/Temporary/LastTest.log
# If you want detailed output on the terminal, please add -V
ctest -R Opts # Test IR transformation passes
ctest -R Long # Test passes that take a lot of time
ctest -R Litmus # Test litmus onlyWe appreciate any kind of contributions to this project!