Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 16:15 - 16:30 at CPP - Compilers and Interpreters Chair(s): Freek Wiedijk

We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 16:45
Compilers and InterpretersCPP at CPP
Chair(s): Freek WiedijkRadboud University Nijmegen

Streamed session: https://youtu.be/TVqCuMMTuos

16:00
15m
Talk
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award
CPP
Magnus O. MyreenChalmers University of Technology
Pre-print Media Attached
16:15
15m
Talk
Lutsig: A Verified Verilog Compiler for Verified Circuit Development
CPP
Andreas LööwChalmers University of Technology
Pre-print Media Attached
16:30
15m
Talk
Towards Efficient and Verified Virtual Machines for Dynamic Languages
CPP
Martin DesharnaisUniversität der Bundeswehr München, Stefan BrunthalerUniversität der Bundeswehr München
Pre-print Media Attached