Synthèse de haut niveau: circuits élastiques formellement vérifiés

Cette séance de cours traite du développement d'un compilateur de synthèse de haut niveau (HLS) formellement vérifié pour les circuits élastiques, qui sont un type de circuit de flux de données. L'instructeur décrit les défis traditionnels de la conception de FPGA, où les outils spécifiques au matériel ont un chevauchement limité avec les outils de conception de logiciels. La séance de cours souligne la nécessité d'un nouveau backend pour le compilateur CompCert qui peut produire des circuits élastiques, abordant la préservation sémantique de la transformation des modèles d'exécution pilotés par le contrôle en modèles pilotés par les données. L'instructeur introduit deux représentations intermédiaires équivalentes (IR) des circuits élastiques et leur sémantique opérationnelle pour faciliter cette transition. La séance de cours couvre également les propriétés des circuits élastiques, telles que l'insensibilité à la latence et la planification dynamique, ainsi que l'importance du déterminisme pour assurer un comportement correct des circuits. La discussion comprend le travail actuel sur la validation de l'IR proposé avec un interprète et les plans futurs pour formaliser les circuits élastiques matériels, en intégrant le temps dans la formalisation. Dans l'ensemble, la séance de cours fournit un aperçu complet du projet et de ses implications pour la conception des circuits.