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.
A formally verified high-level synthesis tool based on CompCert and written in Coq.
My personal Emacs configuration
My personal dotfiles.
Personal blog and website.
Personal Zettelkasten
42ab738 Add incremental evaluability check
~ymherklotz pushed to ~ymherklotz/vericert git
f9511b8 Add better implementation of evaluability
~ymherklotz pushed to ~ymherklotz/vericert git
73d0904 Add timing of scheduling to Compiler.v
~ymherklotz pushed to ~ymherklotz/vericert git
24a34a9 Add new constraints checking
~ymherklotz pushed to ~ymherklotz/vericert git
1850879 Add benchmarking of unhashed commands
~ymherklotz pushed to ~ymherklotz/vericert git
c3edebe Fix documentation generation
~ymherklotz pushed to ~ymherklotz/vericert git
6a74d2e Add unhashed functions for comparisons
~ymherklotz pushed to ~ymherklotz/vericert git
dbc7e04 Mac specific change
~ymherklotz pushed to ~ymherklotz/ymh-emacs git
05a2d29 Add blog and gnuplot and ox-rst
~ymherklotz pushed to ~ymherklotz/ymh-emacs git
c9d0a0b Add Bambu synthesis and ClockRegisters
~ymherklotz pushed to ~ymherklotz/vericert git
557472a Abort steytin proofs
~ymherklotz pushed to ~ymherklotz/vericert git
533bca9 Annonimize submission
~ymherklotz pushed to ~ymherklotz/vericert git
f6569b7 Add comments next to admitted theorems
~ymherklotz pushed to ~ymherklotz/vericert git
4d62c7f Abort steytin proofs
~ymherklotz pushed to ~ymherklotz/vericert git