Efficient, Correct, and Practical High-Level Synthesis

The state-of-the-art in program verification has progressed to the point where a compiler, a complex software artifact, can be verified by a proof assistant with unquestionable mathematical rigor. This subject builds on this state-of-the-art to propose a new target, hardware design for reconfigurable architectures (such as FPGAs), and a new domain, high-level synthesis (HLS), where the compiler produces a custom hardware design with energy-efficient computations, rather than traditional assembly code. To this end, this PhD will initiate a collaboration of experts with complementary profiles on a subject that combines two disciplines, formal methods and architecture. The cooperation will bridge research of a fundamental nature with research of a more applied nature, where we test our technology and tools on realistic case studies.

Focusing on HLS will require the design of new semantic models and proof techniques. Indeed, CompCert, the reference among verified compilers performs only simple optimisations based on basic static analysis techniques and operating on an elementary intermediate representation (IR) for compilers. CompCertSSA extends CompCert with a more expressive IR based on the SSA form. Such an IR can be seen as a means of embedding, directly in the data representing the program to be compiled, rich structural and semantic properties, which can then be exploited by the compiler and the respective proof. CompCertSSA opens the way to new IRs used in state-of-the-art (unverified) compilers, such as gated-SSA (GSA) and its variants. Surprisingly, despite their practical popularity, they are still insufficiently studied semantically. This is in contrast to recent progress in source languages or assembly instruction sets. Bridging the gap between these two ends of the spectrum, by studying the semantic foundations of flagship IRs, is necessary. We also argue that it is a necessity to achieve formal verification techniques that scale up in program size and proof difficulty.

The choice of IRs in a compiler depends on the application domain. In this thesis, we will focus on the formalisation of an IR for HLS, and on advanced verified optimisations operating on this IR, such as loop optimisations and code parallelisation. The GSA form seems to be a good candidate as it will allow verification of relevant optimisations, and because it is already sufficiently close to the dataflow style of hardware design that modern HLS tools commonly adopt, for instance to parallelise code. In addition, concerns have been raised about the reliability of currently available HLS tools, and therefore their suitability for use in safety-critical environments. To date, no viable semantic model is available for GSA. Different issues need to be addressed, beyond simply designing a semantic model for this IR. What are their intrinsic properties? How to ensure these properties at generation? How to ensure their preservation by compilation? What proof or verification principles underlie the chosen IR?