May 2024 - July 2024: Research Intern
CentraleSupélec Rennes Campus, SUSHI Team, Inria
Location: Cesson-Sévigné, France
Supervisor: Pierre Wilke
Project: RISC-V Processor Development
Redesigned RISC-V processor for improved flexibility while maintaining formal verification properties. The main outcome was the HeRVé processor, a pipelined in-order RISC-V processor with:
- Support for interrupts and exceptions
- Implementation of RISC-V Zicsr and Zicntr extensions
- Formal verification of a shadow stack mecanism using Coq and Z3
- Written in Kôika, an EDSL in Coq (~6,760 lines)
Technologies: RISC-V, Kôika, Coq, Z3, Formal Verification, Hardware Description Languages
Repository: GitLab - HeRVé
Links: Internship Report | CPU Pipeline