Mechanized semantics for circuits : from dataflow to hardware (Sémantiques mécanisées de circuits : du flot de données au matériel) Law, Tony - (2026-02-20) / Université de Rennes Mechanized semantics for circuits : from dataflow to hardware Accéder au document :  https://ged.univ-rennes1.fr/nuxeo/site/esupversion...

Langue : Anglais Directeur(s) de thèse:  Blazy, Sandrine Discipline : Informatique Laboratoire :  IRISA Ecole Doctorale : MATISSE Classification : Informatique Mots-clés : Vérification formelle, Calcul par flots de données, Synthèse de haut-niveau Synthèse de haut niveau (informatique) Compilateurs (logiciels)

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 flot 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 representation 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.