Profile picture

Hi! I’m currently a PhD student in the Circuits and Systems group at Imperial College London, supervised by John Wickerson.

My research focuses on formalising the process of converting high-level programming language descriptions to correct hardware that is functionally equivalent to the input. This process is called high-level synthesis (HLS), and allows software to be turned into custom accelerators automatically, which can then be placed on field-programmable gate arrays (FPGAs). An implementation in the Coq theorem prover called Vericert can be found on Github.

I have also worked on random testing for FPGA synthesis tools. Verismith is a fuzzer that will randomly generate a Verilog design, pass it to the synthesis tool, and use an equivalence check to compare the output to the input. If these differ, the design is automatically reduced until the bug is located.

Publications

FCCM '22
Michalis Pardalos, Yann Herklotz, and John Wickerson. Resource sharing for verified high-level synthesis. In 30th IEEE Annual Int. Symp. on Field-Programmable Custom Computing Machines, 2022.
 artifact 
OOPSLA '21
Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal verification of high-level synthesis. Proc. of the ACM on Programming Languages, (OOPSLA), 2021.
[ DOI | artifact | pdf | slides | video ]
FCCM '21
Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. An empirical study of the reliability of high-level synthesis tools. In 29th IEEE Annual Int. Symp. on Field-Programmable Custom Computing Machines, 2021.
[ DOI | artifact | pdf ]
FPGA '20
Yann Herklotz and John Wickerson. Finding and understanding bugs in FPGA synthesis tools. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2020.
[ DOI | artifact | blog | pdf | poster | slides ]

Other Papers and Posters

LATTE '21
Yann Herklotz and John Wickerson. High-level synthesis tools should be proven correct. In Workshop on Languages, Tools, and Techniques for Accelerator Design, 2021.
[ pdf | video ]
FPGA '21
Zewei Du, Yann Herklotz, Nadesh Ramanathan, and John Wickerson. Fuzzing high-level synthesis tools. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2021.
[ DOI | slides ]

Blog

Mon, Dec 21, 2020 | 2800 Words
Introduction to Luhmann's Zettelkasten
Niklas Luhmann’s Zettelkasten is becoming increasingly popular for being a great note taking technique. However, it is often misunderstood as taking notes without any structure, whereas Luhmann actually structured his notes hierarchically, but also allowed for arbitrary links between notes.
Sat, Feb 15, 2020 | 1600 Words
Nix for Coq Development
Nix is a great package manager that can be used to control various complex environments easily, such as Coq development with ocaml extraction with various dependencies.
Tue, Nov 26, 2019 | 1100 Words
MSR PhD Workshop on Next-Generation Cloud Infrastructure
Summary of the microsoft talks and posters presented at the MSR PhD Workshop on Next-Generation Cloud Infrastructure.
Wed, Jun 19, 2019 | 700 Words
Verismith
Verilog Fuzzer to test the major verilog compilers by generating random, valid Verilog.
Sun, Feb 24, 2019 | 500 Words
Realistic Graphics
Environment maps can be used to render objects with realistic lighting by indexing into the map.

Service

Program CommitteePERR'22
Artefact EvaluationPLDI'22 , CGO'22 , OOPSLA'20
SubreviewerFCCM'22 , OOPSLA'21 , FCCM'20

News

2022-03-04Artefact evaluation for PLDI'22.
2022-02-24Invited talk at PEQ'22.
2022-02-07Subreviewer for FCCM'22.
2021-11-24Artifact evaluation for CGO'22.
2021-11-22Present hyperblock scheduling at CAS Group.
2021-09-16Present Vericert at the Formal Methods group at Chalmers.
2021-08-31Paper on Vericert accepted at OOPSLA'21.
2021-05-31Internship with Sandrine Blazy and Delphine Demange on CompCertSSA.
2021-02-05Invited seminar talk for the Celtique project.
2020-12-07Present Vericert in front of CAS Group.
coq1 dsp1 emacs2 fpga3 fsharp1 graphics2 hardware3 haskell1 markdown1 ml1 nix1 synthesis1 verilog1 web1 workshop1 writing1