~ymherklotz

https://yannherklotz.com

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.

~ymherklotz/yannherklotz.com

Personal blog and website.

~ymherklotz/hugo-ymherklotz

Personal hugo theme for yannherklotz.com

~ymherklotz/vericert-docs

Vericert documentation website.

~ymherklotz/dotfiles

Personal dotfiles for linux and macos.

~ymherklotz/fpga20_fubfst

FPGA'20 Fuzzing Paper.

~ymherklotz/fccm21_esrhls

FCCM'21 Fuzzing HLS paper.

~ymherklotz/oopsla21_fvhls

OOPLSA'21 Vericert Paper.

~ymherklotz/emacs-zettelkasten

Simple zettelkasten mode for emacs.

~ymherklotz/verismith

Verilog Fuzzer to test the major simulators and sythesisers by generating random, valid Verilog.

~ymherklotz/vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.