Profile picture

Hi! I’m currently a first year PhD student in the Circuits and Systems group at Imperial College London, supervised by Dr. 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

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 ]

Drafts

  • Yann Herklotz, James D. Pollard, Nadesh Ramanathan and John Wickerson, Formal Verification of High-level Synthesis. [pdf]
  • Zewei Du, Yann Herklotz, Nadesh Ramanathan and John Wickerson, Fuzzing High-Level Synthesis Tools. [pdf]

Blog

December 21, 2020
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.
February 15, 2020
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.
November 26, 2019
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.
June 19, 2019
Verismith
Verilog Fuzzer to test the major verilog compilers by generating random, valid Verilog.
February 24, 2019
Realistic Graphics
Environment maps can be used to render objects with realistic lighting by indexing into the map.

more…

News

2021-02-05Invited seminar talk for the Celtique project.
2020-09-10Artifact review committee at OOPSLA 2020.
2020-06-17Gold medal at PLDI 2020 SRC Presentation.
2020-06-15Student volunteer at PLDI 2020.
2020-02-25Presented Verismith at FPGA 2020.

more…