Dépôt numérique
RECHERCHER

La vérification automatique basée sur un modèle mathématique de réalisation pshysiques de circuits numériques.

Dahmoune, Ouiza (2012). La vérification automatique basée sur un modèle mathématique de réalisation pshysiques de circuits numériques. Thèse. Québec, Université du Québec, Institut national de la recherche scientifique, Doctorat en télécommunications, 208 p.

[img]
Prévisualisation
PDF
Télécharger (1MB) | Prévisualisation

Résumé

Le travail effectué dans le cadre de cette thèse vise la réduction du coût et du temps de vérification d'un circuit numérique ainsi que l'augmentation de la couverture de test. Notre hypothèse est que nous pouvons appliquer une des méthodes de vérification utilisée traditionnellement pour des modèles abstraits, à la version physique du circuit. Ce travail consiste donc en une évaluation expérimentale de notre hypothèse. Toutes nos expériences ont été réalisées sur des prototypes synthétisés sur des cartes FPGAs (Field-Programmable Gate Array). Les résultats de ce travail peuvent être résumés comme suit: 1. Une démonstration de la faisabilité de notre approche : elle étend le vérificateur de modèles TLC (Temporal Logic Checker) pour vérifier la conformité d'une implémentation FPGA par rapport à la spécification mathématique exprimée en TLA+, le langage de spécification "natif' de TLC, il est basé sur TLA (Temporal Logic of Actions). Ce point a fait l'objet de deux publications: [34,60]. 2. Lors de nos travaux nous avons été vite confrontés à un problème de goulot d'étranglement causé par les délais de communication. Nous avons implanté un analyseur d'accessibilité hardware (Hardware Reachability Analyser, HRA). Celui-ci est un circuit spécialisé qui permet l'analyse d'accessibilité du circuit physique alors que le vérificateur TLC analyse celle de l'implémentation de référence. Ce point a aussi fait l'objet de deux publications: [33,36]. Notons que l'analyseur ainsi que le circuit analysé sont sur un même FPGA. Ceci nous facilite la controlabilité ainsi que la visibilité du circuit d'une part et nous permet d'accélérer l'analyse d'autre part. 3. Le troisième et dernier résultat de notre travail consiste en un ensemble de mesures expérimentales sur différentes plates-formes. Elles sont illustrées par des tables pour les 2 exemples du contrôleur d'ascenseur et du micro-contrôleur à 8 bits, PicoBlaze de Xilinx. Nous avons donc développé des outils qui peuvent vérifier la conformité d'une réalisation physique d'un circuit numérique par rapport à sa spécification abstraite. Nous voulions que celle-ci réponde à l'ensemble des critères suivants: • Qu'elle se fasse d'une façon concise en termes mathématiques pour décrire le comportement du circuit, l'ensemble des contraintes auxquelles ce dernier doit obéir et la liste de propriétés qui assurent son bon fonctionnement. • Le comportement dans le domaine abstrait est utilisé, par la suite, comme référence à laquelle est comparé le comportement de la réalisation physique. Le processus de validation consiste à démontrer un homomorphisme entre entités (états et transitions) des deux mondes abstrait et physique. • L'automatisation de la génération de l'ensemble des états, des actions et des entrées (des paramètres). Chaque n-tuple (état, action,paraml,param2, ... ) est soumis à chacune des implémentations abstraite et physique et les sorties respectives sont comparées automatiquement pour détenniner la correspondance. • L'automatisation de la génération de l'ensemble des bancs d'essais et des moniteurs qui se chargent respectivement de la soumission des n-tuples et de la lecture des résultats correspondants. Le vérificateur se charge aussi lui même du test de conformité. Le premier avantage de cette approche est qu'elle associe directement le comportement du circuit physique à celui du modèle mathématique de référence. Elle permet aussi une expansion relativement exhaustive tout en réduisant le temps de vérification et en plus de rehausser le niveau d'abstraction, elle élimine la dure tâche d'apprentissage d'un nouveau paradigme de spécification.

Type de document: Thèse
Directeur de mémoire/thèse: Johaston, Robert de B.
Mots-clés libres: USB2.0; algorithmes
Centre: Centre Énergie Matériaux Télécommunications
Date de dépôt: 22 janv. 2013 16:40
Dernière modification: 12 nov. 2015 21:09
URI: http://espace.inrs.ca/id/eprint/707

Actions (Identification requise)

Modifier la notice Modifier la notice