Resource sharing for verified High Level Synthesis
For my Master’s thesis I worked on implementing a resource sharing optimisation to the Vericert High Level Synthesis compiler.
Vericert is a formally verified, high level synthesis compiler for C. This means it compiles C down to Verilog, a hardware description language, generating hardware that is equivalent to the input C code. The translation is formally verified using the Coq proof assistant. This means it has been mathematically proven to never incorrectly compile a program.
My work was to add an optimisation, resource sharing, making the compiler generate more compact hardware, and prove it correct. I am currently working on completing this proof as part of an Undergraduate Research Opportunity in Imperial College London.
You can read my master’s thesis here
A simulator and testbench written as a university project. Simulates almost all mips-1 instructions, and runs real MIPS-1 binaries. Written in C++.
A Verilog emulator and visualiser for first-year EEE students. This project was part of my year 3 High Level Programming module.
Hardware design tooling is notoriously hard to use, especially for beginners. We tried to make things easier for beginners by giving a way to quickly run and visualize verilog designs without having to deal with tools like Quartus or Vivado.
The simulator is written in F# and covers the structural subset of Verilog (modules, continuous assignment, wires, logic and arithmetic operators). We also created an extension for Visual Studio Code to simplify interaction with the simulator and provide useful features such as intellisense or syntax highlighting.
Kima is a programming language I am currently working on. Its main goal is to explore the practicality and design space of algebraic effects, in a statically typed, mostly-imperative language. In its current form it supports product types (structs) and higher-order functions, while I am currently working on algebraic effects.
Written in Haskell and tested using Hspec and Gitlab CI.
I participated in Google Summer of Code 2020, under the haskell.org organisation. My project was centered around ghcide, a project which gives editors IDE-like capabilities for Haskell code, using the Language Server Protocol. I introduced tracing into this software to facilitate profiling its performance.
The project was completed and the functionality was included in the project. This required me to dive deep into the internals of the Haskell compiler (GHC) to be able to measure the size of Haskell objects in memory, and resulted in merging a patch to GHC. As I used OpenTelemetry to implement the tracing feature, I also contributed to the haskell OpenTelemetry library