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. However, unlike Alive2, we focus on supporting dialects that are tailored for compiling machine learning applications only.
Currently MLIR-TV is in an experimental stage.
How to build MLIR-TV
Prerequisites: CMake(>=3.15),
MLIR,
Python3,
Solvers (at least one of them must be used):
z3-4.8.13 ,
cvc5-0.0.3(limited support)
- Installation of MLIR: please follow this instruction & run
cmake --build . --target install
mkdir build
cd build
# At least one of -DZ3_DIR and -DCVC5_DIR should be set. Build will fail otherwise
# -DUSE_LIBC is OFF by default. Set it to ON iff the MLIR (and CVC5) is linked against libc++
cmake -DMLIR_DIR=<dir/to/mlir-install> \
[-DZ3_DIR=<dir/to/z3-install>] \
[-DCVC5_DIR=<dir/to/cvc5-install>] \
[-DUSE_LIBC=ON|OFF] \
[-DCMAKE_BUILD_TYPE=DEBUG|RELEASE] \
..
cmake --build .How to run MLIR-TV
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=5000How to test MLIR-TV
cd build
# A detailed log is written to build/Testing/Temporary/LastTest.log
# If you want detailed output on the terminal, please add -V
# ctest -R Unit # Currently unavailable
ctest -R Opts # Test IR transformation passes
ctest -R Long # Test passes that take a lot of time
ctest -R Litmus # Test litmus only