Sémantique formelle d’une infrastructure de compilation matériel

Publié le : 12 mars 2020

Le développement du jeu d’instruction RISC-V est supporté par la conception et l’utilisation de nouvelles méthodes et outils dédiés à l’augmentation du niveau de productivité de la conception d’architectures matérielles (i.e. langage de plus haut niveau pour la conception matériel et chaîne de compilation spécialisée). Au niveau langage, les langages de description matériel tels que Chisel et FIRRTL ont pour but d’augmenter le niveau d’abstraction utilisé dans la conception d’architectures matérielles. Il devient donc intéressant et nécessaire de raisonner formellement sur les propriétés fonctionnelles et temporelles de ces conceptions matérielles exprimées à plus au haut niveau et de s’appuyer sur des extensions appropriées de l’infrastructure de compilation matériel pour transférer ces propriétés de haut niveau vers, par exemple, le code Verilog généré.

Dans cette proposition de thèse, nous visons la définition d’un environnement de vérification des architectures matérielles permettant de spécifier et vérifier des propriétés de sécurité mais aussi de sûreté temporel. Les deux contributions attendues de ce thèse sont : 1) la conception et l’implémentation d’une infrastructure de vérification basée sur une sémantique formelle exécutable des langages Chisel et FIRRTL et 2) la conception et l’implémentation d’un langage d’assertion pour exprimer des propriétés de sécurité et de sûreté temporel qui seront ensuite vérifiées sur l’infrastructure formelle développée précédemment. Les contributions scientifiques de cette thèse seront évaluées sur une sélection d’architectures matérielles issues du riche eco-système RISC-V.

En naviguant sur notre site, vous acceptez que des cookies soient utilisés pour vous proposer des contenus et services adaptés à vos centres d’intérêts. En savoir plus
X