Dissertation

Certified Software for Designing Asynchronous Circuits August 2020 [pdf] [code]
Committee: Ross Tate, Rajit Manohar, Hakim Weatherspoon, Bob Constable

I used Coq to mechanically formalize the semantics of CHP (Communicating Hardware Processes, a high-level language used to design asynchronous circuits) and build a certified CHP simulator.

Publication

Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications PLDI 2015 [downloads]
Authors: Stephen Longfield, Brittany Nkounkou, Rajit Manohar, Ross Tate

I used Coq to mechanically prove that our newly developed CHP semantics used in our CHP-error-detection tool are equivalent to the commonly accepted CHP semantics.