Tobias Grosser
JoinTeamVisionProjectsPublicationsContact

Formal Verification at the Soft and Hardware Boundary

Start: Anytime 2022/23

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.

You are ...

  • passionate about research and exploring novel ideas.
  • have a BSc or MSc in computer science, maths, electrical engineering, or related areas.
  • excited about open-source software and develop formal theory.
  • curious to learn and explore the tools discussed above (no need for extensive previous experience).

We offer

  • funding for a PhD position at the University of Edinburgh (tuition and cost of living)
  • freedom to develop your own research agenda
  • collaboration with the RISC-V and CIRCT community:
    • Martin Berger (Huawei) as SAIL for RISC-V maintainer
    • Fabian Schueki (SiFive) as LLHD maintainer and CIRCT contributor
  • Tobias' support in delivering excellent research with real-world impact
  • Tobias' personal commitment to an open and supportive research environment where diversity and well-being is seen as foundational for excellent research.

To get started, write me an informal email and I will guide you through the application process!

Check also our other job openings.