on November 24, 2025 at 3:30 pm
Titre : Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
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’ordonne 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.
More...Salle Turquoise, Bâtiment ESPRIT, CRIStAL
français
English