Publications

Thèses


< retour aux thèses

« Assertions et conception matérielle ».

Auteur : K. Morin-Allory
Président du jury : H. Garavel
Rapporteur(s) de thèse : B. Rouzeyre, R. De Simone, J.-P. Talpin,
Examinateur(s) de thèse : D. Borrione,
HDR Université de Grenoble
Spécialité : Architecture des systèmes
Soutenance : 15/11/2018
ISBN : 978-2-11-129246-8

Résumé

Les travaux développés dans cette portent sur la vérification, la synthèse et la compréhension d'un circuit à partir d’assertions temporelles. Les assertions sont exprimées dans le langage PSL (Property Specification Language). Dans ce document, nous proposons une interprétation matérielle de la sémantique de ce langage : à chaque opérateur PSL (aussi bien de type LTL que de type expression régulière) est associé un circuit appelé réactant primitif. L’interconnexion de ces réactants primitifs permet de construire deux types de circuits : des observateurs ou des réactants. Les observateurs sont des circuits chargés de vérifier en cours de fonctionnement (simulation, émulation, en ligne) si une propriété temporelle est ou non satisfaite. Les réactants sont des circuits implémentant une spécification PSL en matériel : c’est une synthèse sous forme matérielle de la spécification. Tous les circuits obtenus sont corrects par construction et ont été implémentés sur carte FPGA. La méthode proposée ici est modulaire, et contrairement à la littérature existante, ne s’appuie ni sur les automates ni sur la théorie des jeux. Par ailleurs, la synthèse de la spécification permet de comprendre son fonctionnement en générant des chronogrammes, en vérifiant qu’elle est complète et cohérente.