I’m currently a postdoc with Thomas Bourgeat in the Verification and Computer Architecture (VCA) lab at EPFL, working on marrying interactive theorem provers with hardware verification. Before that I did a PhD 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
- PLDI '24
- Yann Herklotz and John Wickerson.
Hyperblock scheduling for verified high-level synthesis.
Proc. of the ACM on Programming Languages, (PLDI), 2024.
[ DOI | artefact | pdf ] - CPP '23
- Yann Herklotz, Delphine Demange, and Sandrine Blazy.
Mechanised semantics for gated static single assignment.
In Proc. of the 12th ACM SIGPLAN Int. Conf. on Certified
Programs and Proofs (CPP), 2023.
[ DOI | artefact | pdf | slides ] - 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 (FCCM), 2022.
Short paper, HIPEAC 2022 Paper Award.
[ DOI | artefact | pdf ] - 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 | artefact | blog | changelog | pdf | poster | 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 (FCCM), 2021.
Short paper.
[ DOI | artefact | 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
(FPGA), 2020.
[ DOI | artefact | 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 ]
Thesis
- PhD Thesis
- Yann Herklotz Grave.
Formal Verification of High-Level Synthesis.
PhD thesis, Imperial College London, UK, April 2024.
[ artefact | pdf ] - Masters Thesis
- Yann Herklotz Grave.
Fuzzing Verilog.
Masters thesis, Imperial College London, UK, June 2019.
[ artefact | pdf ]
Blog
Service
Program Committee | LATTE'23, PERR'22 |
Artefact Evaluation | ECOOP'23, PLDI'22, CGO'22, OOPSLA'20 |
Subreviewer | POPL'24, ECOOP'23, FCCM'22, OOPSLA'21, FCCM'20 |
News
2024-04-19 | Defended my PhD thesis in front of Xavier Leroy and George Constantinides. |
2024-02-13 | Submitted my PhD thesis. |
2024-01-14 | Attended POPL'24 in London. |
2023-12-01 | Started as a postdoc with Thomas Bourgeat in the VCA lab. |
2023-01-16 | Presented our CPP'23 paper in Boston. |
2022-12-19 | Internship at Amazon in the Prime Video Automated Reasoning Group. |
2022-10-31 | Present verified GSA semantics at CAS Group. |
2022-08-12 | Talk at the Concurrency Meeting 2022 about Formalising Predicated Execution. |
2022-06-28 | Program Committee for PERR'22. |
2022-06-17 | Presented the OOPSLA'21 paper at PLDI'22. |
more... |