Université de Rennes Mechanized semantics for circuits : from dataflow to hardware Sémantiques mécanisées de circuits : du flot de données au matériel Vérification formelleCalcul par flots de donnéesSynthèse de haut-niveau Formal VerificationDataflow ComputationHigh-Level Synthesis Synthèse de haut niveau (informatique) Compilateurs (logiciels) 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 1767 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/684b9cc7-f089-49fc-b5a4-4309ca2716e4 Law Tony 1999-08-07 FR 297332384 pro@tnlw.fr 2026URENS010 http://www.theses.fr/2026URENS010 2026-02-20 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiBlazySandrineintervenant_1153042567PuautIsabelleintervenant_2071169733DerrienStevenintervenant_3069997519DemangeDelphineintervenant_4174231989BourgeatThomasintervenant_729733283XDagandPierre-Evaristeintervenant_5253134765WickersonJohnintervenant_6297332546 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 BlazySandrinePuautIsabelleDerrienStevenDemangeDelphineDagandPierre-EvaristeWickersonJohnBourgeatThomasUniversité de RennesMATISSE IRISA ASCII PDF 1808933