To design trustworthy solutions we need both trustworthy hardware and software. Formal proof techniques are to be applied to the full stack from software on the top to hardware at the bottom. Only then will we succeed in building really trustworthy systems.
Designing correctly working hardware and software is a hard and tricky business to say the least. For example, designing correct Chiplets is already difficult, but ensuring they work together and interact in the intended way is more difficult still. Another example is the difficulty of writing microcode after designing an ISA, and guaranteeing the translation to be correct. Well-publicized calamities include the classic FDIV-bug, and much more recently Spectre and Meltdown.
Much progress is to be expected from a natural combination of two technologies that have both seen a dramatic increase in quality and productivity during the past few years.
In the first place, we need Interactive Theorem Provers (ITPs). Although formal methods such as verification with ITPs like Rocq or HOL are now routinely deployed, they are not used at large and only on separate parts during development. We propose a more integrated, full-stack verification which is now within reach of current ITPs thanks to their much increased capabilities during the past 5 years.
However, the manual part of proving correctness is still significant, and here the second technology comes into play. Artificial Intelligence has seen a big leap in the past years with the massive breakthrough of Large Language Models (LLMs). Nowadays, these LLMs are trained on formal proofs from ITPs, and can assist proof-building in unprecedented ways, paving the way for fast verification of large and complex designs.
Objectives
In this PhD-thesis we will combine ITPs and LLMs to automate the process of generating correct hardware designs, starting from the high-level abstract behavioral specification of a digital system and generating a register-transfer level description that realizes the abstract specification. This high-level synthesis (HLS) consists of many different steps, from the abstract to the concrete, each of which has to be verified for correctness. By chaining the proofs we obtain the formal verification of a correct translation.
Thus, the work breaks down in two main parts:
1- Standard industry tools for designing hardware and interactive theorem provers use different formal languages. A common language has to be designed to so they can function seamlessly as one tool.
2- We have to automate the proofs that are needed to verify the correctness of the synthesis of the abstract specification to the concrete realization of the design.
Current industrial tools to assist in this proces fall short in one or more of several ways; e.g. they focus on only one layer instead of the full stack, they require tedious and hand-written specifications, they require intensive effort to obtain the accompanying proofs, they focus on coverage checking instead of formal mathematical proofs, and so on. Our envisioned one-stop-shop tool will assist verified HLS with AI-generated proofs, ensuring correct and verified results.