BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cambridge Compiler Social Talks - Mathieu Fehr\, Martin Erhart
DTSTART:20241204T160000Z
DTEND:20241204T170000Z
UID:TALK225247@talks.cam.ac.uk
CONTACT:Luisa Cicolini
DESCRIPTION:Formal Semantics for MLIR Dialects - Mathieu Fehr\n\nMLIR 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 mo
 dular and extensible\, allowing for the definition of custom IRs. However\
 , MLIR is primarily focused on syntax\, and does not provide a way to defi
 ne the semantics of operations in a formal way. This makes it difficult to
  reason about the correctness of transformations and analyses\, and is a b
 arrier to the development of formal verification tools for MLIR-based comp
 ilers. In this talk\, we will introduce a set of semantics dialects\, base
 d 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 diale
 cts to give semantics of core MLIR dialects\, such as arith\, comb\, and m
 emref\, and how we can use this new abstraction to define formal verificat
 ion tooling such as a translation validation tool\, a peephole rewrite ver
 ifier and synthetizer\, and a dataflow analysis verifier.\n\nArcilator: fa
 st and cycle-accurate hardware simulation in CIRCT - Martin Erhart\n\nArci
 lator 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 propriet
 ary simulator. It supports all frontend languages that are fully lowered t
 o 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. Mo
 reover\, we will show that it already delivers performance comparable to V
 erilator\, and explore future developments of Arcilator.\n\nFind out more 
 on: https://grosser.science/compiler-social-2024-12-04/
LOCATION:Computer Laboratory\, William Gates Building\, LT1
END:VEVENT
END:VCALENDAR