High-Level Synthesis: Formally Verified Elastic Circuits

This lecture discusses the development of a formally verified high-level synthesis (HLS) compiler for elastic circuits, which are a type of dataflow circuit. The instructor outlines the traditional challenges in FPGA design, where hardware-specific tools have limited overlap with software design tools. The lecture emphasizes the need for a new backend for the CompCert compiler that can produce elastic circuits, addressing the semantic preservation of transforming control-driven execution models into data-driven ones. The instructor introduces two equivalent intermediate representations (IR) of elastic circuits and their operational semantics to facilitate this transition. The lecture also covers the properties of elastic circuits, such as latency insensitivity and dynamic scheduling, and the importance of determinism in ensuring correct circuit behavior. The discussion includes the current work on validating the proposed IR with an interpreter and future plans to formalize hardware elastic circuits, embedding time within the formalization. Overall, the lecture provides a comprehensive overview of the project and its implications for circuit design.