Formal Semantics for MLIR Dialects - Mathieu Fehr
MLIR is a recent compiler infrastructure project that aims to provide a
unified way of defining SSA compiler IRs and transformations. It is designed
to be modular and extensible, allowing for the definition of custom IRs.
However, MLIR is primarily focused on syntax, and does not provide a way to
define the semantics of operations in a formal way. This makes it difficult
to reason about the correctness of transformations and analyses, and is a
barrier to the development of formal verification tools for MLIR-based
compilers.
In this talk, we will introduce a set of semantics dialects, based on SMT-LIB,
which allows to define the semantics of MLIR dialects as a compiler transformation.
We will show how we can use these semantics dialects to give semantics of core
MLIR dialects, such as arith, comb, and memref, and how we can use this
new abstraction to define formal verification tooling such as a translation
validation tool, a peephole rewrite verifier and synthetizer, and a dataflow
analysis verifier.
Mathieu Fehr is a final-year PhD student at the University of Edinburgh,
currently visiting at the University of Cambridge. A large part of his research
focuses on improving the accessibility of compiler technology, which
includes the design and development of xDSL, a smoother entry-point for
MLIR. His broader research interests encompass advancing declarative
approaches in compiler design to facilitate formal reasoning and enable an
ecosystem of compilation tools, including verifiers, fuzzers, and
superoptimizers.
Arcilator: fast and cycle-accurate hardware simulation in CIRCT - Martin Erhart
Arcilator
is a cycle-accurate hardware simulator in CIRCT that eliminates the
need to export the design to Verilog and use a third-party OSS or
proprietary simulator. It supports all frontend languages that are fully
lowered to CIRCT's core representation, currently including Chisel and a
subset of SystemVerilog. We will discuss the design and implementation
of Arcilator and the novel IR that connects CIRCT's core representation
to LLVM IR. Moreover, we will show that it already delivers performance
comparable to Verilator, and explore future developments of Arcilator.
Martin
Erhart is a Senior Engineer at SiFive working on compilers for hardware
design and verification. He got his MSc in Computer Science at ETH
Zurich, and has gained valuable experience in compiler research and
development through internships with Google Research, SiFive, and Oracle
Labs, in addition to his academic endeavors. Martin has been actively
contributing to CIRCT since its inception.
