February 2025 - July 2025: Visiting Student
Imperial College London, Department of Electrical and Electronic Engineering
Location: London, UK
Supervisor: John Wickerson
Project: Verilog Expression Typing
Worked on formal methods for SystemVerilog bit-width inference using bidirectional typing with IEEE 1800 compatibility. The project involves:
- Developing a formal framework for SystemVerilog bit-width inference
- Creating mechanized proofs in Rocq with formal equivalence guarantees to the existing standard
- Implementing a linear-time reference algorithm with standardization proposal addressing specification ambiguities
Technologies: SystemVerilog, Formal Methods, Bidirectional Typing, Rocq (Coq)
Repository: GitHub - Verilog Typing
Links: Research Paper | Rocq Proofs | Standardization Proposal