MLIR-TV project

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.

This project is published at CAV'22 (link).

How to build MLIR-TV

Prerequisites: CMake(>=3.13), MLIR, Python3,
Solvers (at least one of them must be used): z3-4.8.13 , cvc5-1.2.0

Optional prerequisites: Ninja

Building dependencies

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.

Z3. Please build Z3 using CMake and install it to somewhere designated by CMAKE_INSTALL_PREFIX.

cvc5. Download the binary release (shared libs) and extract the compressed files.

Building MLIR-TV

cmake -Bbuild \
      # We recommend to 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 -j

How to run MLIR-TV

MLIR-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=5000

How to test MLIR-TV

cd 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 Litmus # Test litmus only
ctest -R Opts # Test IR transformation passes
ctest -R Long # Testcases that take a lot of time

Contributions

We appreciate any kind of contributions to this project!