Projects

Vericert

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.

This work was published as a short paper in FCCM 2022. You can read the paper here

You can read my master’s thesis here

The Kima Programming language

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.

Verishot

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.

MIPS Simulator

A simulator and testbench written as a university project. Simulates almost all mips-1 instructions, and runs real MIPS-1 binaries. Written in C++.