Tobias Grosser

Formal Verification at the Soft and Hardware Boundary

Start: September 2021

Are you finishing your degree? Do you feel excited about formal methods, hardware design, and programming languages? Does collaborating with an international team on open-source software used to design real hardware sound interesting to you?

CPU Die

I am looking for a PhD student who is interested in bringing formal methods and automatic verification into the CIRCT open-source hardware design stack. Only two years ago, we introduced with LLHD a Verilog compiler that uses open-source to make the hardware design software stack accessible to everybody. At the same time Sail was introduced as a high-level specification framework and verification framework for describing the HW/SW boundary fully rigorously. Sail is currently the official language for RISC-V, the first fully open source processor ISA. We meanwhile joined forces with Xilinx, SiFive, and many others to create the open-source CIRCT project. CIRCIT is aimed to seed an entire ecosystem of open-source hardware design abstractions that makes the development of open-source hardware (e.g., RISC-V) easy and effortless.

In this project, we will develop formal techniques that allow us to provide strong guarantees about correctness at the soft and hardware boundary. We aspire to develop SSA-based compiler abstractions in MLIR, develop formal semantics in frameworks such as LEAN and Sail, or use SMT solvers and bounded model checking to automatically proof various hardware and software properties as well as properties at the interface between software and hardware. We will also use type-theory, e.g. to introduce dependent types into compiler frameworks such as MLIR. Our objective is reduce verification times from days to minutes and to make automatic verification as easy to us as code-completion in your text editor.

About you:

  • Passionate about research and exploring novel ideas
  • BSc or MSc in computer science, mathematics, electrical engineering, or related background
  • Excited to write software and develop formal theory
  • Curious to learn and explore (some of) the techniques and tools discussed above (you do not need to have previous experience in all areas covered in this project).

What I can offer:

  • Funding for a PhD position at the University of Edinburgh (tuition and cost of living)
  • Freedom to develop and explore your own research agenda
  • Close collaboration with the RISC-V and CIRCT community, e.g., Martin Berger (Huawei) as SAIL for RISC-V maintainer, Fabian Schueki (SiFive) as LLHD maintainer and CIRCT contributor, and the overall CIRCT community.
  • My time to guide and support you in delivering excellent research with real-world impact
  • My personal commitment to an open and supportive research environment where diversity and well-being are not an afterthought, but seen as

critical foundations for excellent research.

If you are potentially interested in this position, write me an informal email and I am happy to guide you through the application process!

I currently have funding for a UK-based student. If you are an international student, talk to me and I am hopeful that I can acquire further funding for you.