Room 206 (2nd floor, badged access)
13 novembre 2025 - 15h00
Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
par Yann Herklotz de VCA lab at EPFL (CH)
invité(e) par David MONNIAUX
13 novembre 2025 - 15h00
Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
par Yann Herklotz de VCA lab at EPFL (CH)
invité(e) par David MONNIAUX
Résumé : Les entreprises de design hardware passent plus de 60% de leur temps uniquement à vérifier que les puces qu'elles conçoivent fonctionnent comme prévu. Face à la montée en complexité et en besoins des accélérateurs hardware personnalisés, les designers travaillent sur le hardware à différents niveaux d'abstraction. Cependant, la vérification elle-même est généralement effectuée directement sur le hardware final.
Pour améliorer cette situation, je propose deux outils de synthèse de haut niveau (HLS) formellement vérifiés, appelés Vericert et Graphiti, qui génèrent deux types différents de designs hardware à partir de spécifications haut niveau écrites en C. Vericert ordonne statiquement les instructions afin de trouver du parallélisme au niveau des instructions dans des hyperblocks (un ensemble de blocs basiques sans boucles). Graphiti, en revanche, génère des circuits avec des composants insensible à la latence qui s'ordonnes pendant l'exécution. Ce circuit correspond directement à la représentation en graphe de flot de données du programme, et les optimisations sont effectuées via des réécritures sur ce graphe.
Je montre que ces deux outils sont comparables aux outils existants de HLS non vérifiés, et j'explore en particulier comment la réécriture de graphes peut aider à raisonner sur le hardware et favoriser la création d'un écosystème de vérification plus adapté à l'échelle.
NB: potentiel candidat CR CNRS
