Publications

Thèses


< retour aux thèses

« Synthèse automatique de circuits numériques à partir de spécifications temporelles ».

Auteur : N. Javaheri
Directeur de thèse : D. Borrione
Co-directeur de thèse : K. Morin-Allory
Président du jury : Ph. Coussy
Rapporteur(s) de thèse : P. Prinetto, R. Drechsler,
These de Doctorat Université de Grenoble
Spécialité : Nanoélectronique et Nanotechnologies
Soutenance : 01/10/2015
ISBN : 978-2-11-129199-7

Résumé

Les travaux présentés dans cette thèse vise à automatiquement communication et contrôle prototypes de spécifications temporelles d´eclaratives. D’un ensemble de propriétés PSL, nous produisons un synthetisable RTL automatiquement. La méthode proposée est modulaire, contrairement aux méthodes publiées antérieurement qui étaient fondées sur la théorie des automates. De chaque propriété, nous produisons un composant qui observe certains opérandes et génère des formes d’onde pour les autres opérandes : le réactif.
Tout d’abord, une bibliothèque des réactifs primitives a été fournie pour les opérateurs FL et SERE. A cet objectif, une relation de dépendance est définie pour chaque opérateur qui exprime la dépendance entre les opérandes de type à l’aide de la sémantique de l’opérateur. Ensuite, la relation de dépendance de chaque opérateur est interprétée comme un composant matériel qui implémente l’opérateur : réactif primitif de l’opérateur.
A l’aide de cette formalisation, on propose une méthode pour déterminer automatiquement quels signaux d’une propriété sont observés et qui sont générés. Dans les cas lorsque précisant le sens du signal n’est pas possible, un solveur est implémenté pour identifier la valeur de signal. En outre, la façcon de déterminer la valeur du signal généré dans plusieurs de ses propriétés est adressée. Le circuit final est l’interconnexion de réactifs et de résoudre les propriétés.
Un prototype d’outil SyntHorus2, qui est une extension d’HORUS, a été mis au point. Il prend les propriétés PSL comme ses entrées et génère le code VHDL synthétisable du circuit. En outre, il génère des propriétés complémentaires pour vérifier si l’ensemble des spécifications est cohérent et complet. La méthode est efficace et synthétise les circuits de commande en quelques secondes. Résultats obtenus sur les repères classiques montrent que notre technique compile propriétés plus efficace que les précédents outils de prototype.

pdf pdf