Cambridge Compiler Social Talks

Add to your list(s) Download to your calendar using vCal

• Mathieu Fehr, Martin Erhart
• Wednesday 04 December 2024, 16:00-17:00
• Computer Laboratory, William Gates Building, LT1.

If you have a question about this talk, please contact Luisa Cicolini.

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.

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.

Find out more on: https://grosser.science/compiler-social-2024-12-04/

This talk is part of the lc985's list series.

This talk is included in these lists:

• Computer Laboratory, William Gates Building, LT1

Note that ex-directory lists are not shown.