Soutenance de thèse de Tony Law vendredi 20 février 2026 à 14h00 en salle Petri-Turing

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse qui aura lieu le vendredi 20 février 2026 à 14h00 en salle petri-Turing ainsi qu'au pot qui suivra en salle Sein.

Titre : "Sémantiques mécanisées de circuits : du flot de données au matériel"/"Mechanized Semantics for Circuits : From Dataflow to Hardware"

Résumé :

La synthèse de haut-niveau (HLS) est une méthode pour produire une description de matériel à partir d’une spécification haut-niveau, en général écrite en C. Elle fait ainsi intervenir deux modèles d’exécution différents : en entrée, des programmes séquentiels dirigés par leur flot de contrôle, et en sortie, des circuits parallèles dirigés par leurs flots de données. Des techniques d’ordonnancement dynamique permettent d’exploiter le parallélisme du matériel lors de la transition entre ces deux modèles.
Cette thèse est un premier pas dans la conception d’un compilateur HLS à ordonnancement dynamique, formellement vérifié dans l’assistant de preuve Rocq. Notre travail se concentre sur une représentation de circuits permettant ce dynamisme, les circuits flots de données, que nous formalisons à deux niveaux : leur spécification au niveau flots de données, et leur implémentation au niveau matériel. Nous étudions deux vues équivalentes de ces circuits : une représentation graphique naturellement adaptée pour les compilateurs, et un langage inductif facilitant les raisonnements et nous permettant ainsi de prouver des méta-propriétés sémantiques, notamment la préservation sémantique. Nous testons la validité de notre travail par rapport à Dynamatic, un outil HLS à ordonnancement dynamique utilisant ces mêmes circuits.

Abstract :

High-level synthesis (HLS) is a method in which a hardware design is produced from a high-level specification, generally written in C. It thus involves two different execution models: as inputs, sequential programs driven by their control flow, and as outputs, parallel circuits driven by their data flows. Dynamic scheduling techniques improve the use of hardware parallelism when transitioning between both models.
This thesis is a first step in the design of a dynamic-scheduling HLS compiler, formally verified in the Rocq proof assistant. Our work focuses on a circuit reprensentation that enables such dynamism, dataflow circuits, which we formalize at two levels: their specification at dataflow level, and their implementation at hardware level. We study two equivalent views for circuits: a graphical representation naturally suitable for compilers, and an inductive language simplifying reasonings and letting us prove semantic meta-properties, notably semantic preservation. We test the validity of our work against Dynamatic, a dynamic-scheduling HLS tool that also uses dataflow circuits.