Sorry, this entry is only available in Français.

Conception rigoureuse de circuits basée sur les méthodes formelles

Présentation du sujet

Dans un premier temps, le travail consistera à étudier HPDcache, un cache de données L1 hautes performances compatible avec les processeurs RISC-V. HPDcache est utilisé dans l’implémentation CVA6 du RISC-V utilisé par plusieurs industriels. Il s’agit d’un cache hautement configurable, avec exécution dans le désordre (out-of-order) et reexécution (replay), muni d’interfaces compatibles avec AMBA AXI5 et RISC-V. L’étude du HPDcache sera faite en construisant un modèle formel de son architecture, qui comporte un pipeline à trois étages, permettant de traiter environ 10 transactions simultanées. Plusieurs configurations seront considérées, en fonction des différentes fonctionnalités activées du HPDcache. Ce modèle formel servira de base pour vérifier des propriétés de correction (absence de livelocks et de deadlocks, respect du modèle de cohérence du processeur, etc.), pour générer des tests de conformité et pour estimer les performances du cache. Dans un deuxième temps, le travail consistera à proposer des extensions de la méthodologie de conception des circuits avec des méthodes formelles (modélisation, vérification, test de conformité), notamment en considérant les architectures à composants communicants (chiplets). Une partie intéressante de cette méthodologie pourrait être des passerelles entre les langages de description de ces circuits et de leurs protocoles de communication sous-jacents et les langages formels utilisés pour la vérification.