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

https://yannherklotz.com

vericert

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

ymh-emacs

My personal Emacs configuration

dotfiles

My personal dotfiles.

yannherklotz.com

Personal blog and website.

zk

Personal Zettelkasten

Activity

42ab738 Add incremental evaluability check

5 days ago via vericert

f9511b8 Add better implementation of evaluability

8 days ago via vericert

73d0904 Add timing of scheduling to Compiler.v

8 days ago via vericert

24a34a9 Add new constraints checking

8 days ago via vericert

1850879 Add benchmarking of unhashed commands

12 days ago via vericert

c3edebe Fix documentation generation

13 days ago via vericert

6a74d2e Add unhashed functions for comparisons

13 days ago via vericert

dbc7e04 Mac specific change

a month ago via ymh-emacs

05a2d29 Add blog and gnuplot and ox-rst

a month ago via ymh-emacs

c9d0a0b Add Bambu synthesis and ClockRegisters

a month ago via vericert

557472a Abort steytin proofs

a month ago via vericert

533bca9 Annonimize submission

a month ago via vericert

f6569b7 Add comments next to admitted theorems

a month ago via vericert

4d62c7f Abort steytin proofs

a month ago via vericert

399a781 macos changes

a month ago via dotfiles
1 / 48