~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.

vericert

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

yannherklotz.com

Personal blog and website.

emacs-zettelkasten

Simple zettelkasten mode for emacs.

dotfiles

My personal dotfiles.

choc

An implementation of the Calculus of Construction.

Activity

b3e2078 Famous proven but not tested has been fixed

10 days ago via vericert

b3e2078 Famous proven but not tested has been fixed

10 days ago via vericert

3113194 Completely finish RTLBlockgenproof

10 days ago via vericert

4c87dd3 Up to Icall is now proven

10 days ago via vericert

ab45ed9 Try to expand the definition of match_code

11 days ago via vericert

92548d1 Finish Inop proof for basic block generation

12 days ago via vericert

274cb94 Add new definitions of match_code

12 days ago via vericert

6019989 Change the specification of the RTLBlockgenproof

14 days ago via vericert

a3b64c3 Try to work on refining the match_states predicate

16 days ago via vericert

87b8ba3 Remove first-letter shenanigans

18 days ago via yannherklotz.com

46b997b Reset social size

18 days ago via yannherklotz.com

f1b2d11 Subdue the color and fix the CSS

19 days ago via yannherklotz.com

e66e492 Change the links

19 days ago via yannherklotz.com

603a5b6 Add new entry to Changelog

20 days ago via emacs-zettelkasten

92a070f Add export date to notes

20 days ago via emacs-zettelkasten
1 / 13