PV1 ⊧ mlir-tvchecks correctness of transformations for MLIR

Application domain/field

• Machine learning compilers
• Compilers
• Translation validation
• Multi-Level IR (MLIR)

Type of tool

Translation validator

Expected input

Two MLIR functions of identical signatures. One before compiler optimisations and one after compiler optimisations.

Format:

.mlir files

Expected output

Whether the compiler transformation is correct or incorrect. If it is incorrect then it will also find a counterexample.

Internals

This is a translation validation framework for Multi-Level IR. Multi-Level IR (MLIR) is a framework for supporting the development of domain-specific compilers by sharing intermediate representations (IRs). Translation validation aims to check whether a compilation is correct by looking at the input (source program) and output (target program). mlir-tv specifically targets intraprocedural transformations, i.e. functions in the two programs with the same signature are checked pairwisely. Uses Z3