by Martin Berger, University of Sussex
On March 27th, at 11:00 am in room FC6 029 of the DCC-FCUP, Martin Berger will give a talk entitled "Pydrofoil: Compiling Formal Semantics of Processors to Fast Software Models."
The talk is organized by the DCC-FCUP.
Short Bio
Martin Berger is an Associate Professor in the Department of Informatics at the University of Sussex. His research focuses on programming languages, verification, logic, and security. Website: https://users.sussex.ac.uk/~mfb21/
Title
Pydrofoil: Compiling Formal Semantics of Processors to Fast Software Models
Abstract
A processor's functionality is defined by its instruction set architecture (ISA), which specifies the machine language interpreted by the hardware. Accurate and comprehensive ISA specifications are essential for processor design, compiler development, and verification. Instruction set simulators (ISSs), also called functional models, provide software-based models of processor behavior. The efficiency of ISS execution directly impacts processor development speed and associated costs. Traditionally, ISSs were manually implemented, a process that becomes increasingly time-consuming and error-prone as ISA complexity grows. To address this scalability challenge, architecture definition languages (ADLs) have emerged, enabling the automated generation of ISSs from formal ISA descriptions. Many older and widely used ADLs, such as SystemC, extend beyond the pure ISA specification to incorporate microarchitectural details, including pipelining information. This integration, while providing comprehensive modeling capabilities, typically uses low-level language constructs, such as classes and macros, like C++, which introduces complexity into the specification and verification process. Recent years have seen the rise of high-level DSLs for ISA description, in particular Sail (https://github.com/rems-project/sail), which has become the official specification language for RISC-V (https://github.com/riscv/sail-riscv/tree/master/model). However, the Sail-generated ISS is very slow. In this talk, we show how to use a tracing-JIT compiler to compile from Vela to an ISS and achieve >230x speedup. Draft paper: https://arxiv.org/abs/2503.04389