Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
Colloque
En cet article, on propose une approche hiérarchique pour la modélisation et la vérification formelle d’un système embarqué complet à des niveaux élevés d’abstraction, en utilisant les graphes de décision MDG (Multiway Decision Graphs). L’approche est sur une application de contrôleur de souris roulant sur un microcontrôleur commercial (PIC 16C71). Le système est modélisé à différents niveaux de la hiérarchie de conception c.-à-d., le niveau matériel du microcontrôleur, l’architecture de jeux d’instruction du microcontrôleur (ISA), le niveau de code assembleur de logiciel embarqué et la spécification de comportement du logiciel. L’exactitude de la plateforme matérielle d’assembleur de l’architecture destinée est …
Colloque
Avec la complexité de plus en plus croissante des circuits séquentiels, la réutilisation des blocs de circuits ayant une fonctionnalité connue et ayant passé des tests de conformité formels et exhaustifs est de plus en plus une pratique courante, voire indispensable. Notre travail se situe dans le cadre d'implémentation de signature "fonctionnelle" dans les circuits séquentiels prouvant la propriété intellectuelle. Notre contribution est la détermination des tailles minimales, en bits, du codage des variables d'états, d'entrées et de sortie nécessaires pour répondre à des contraintes de probabilité de fausses identifications prédéfinie. Une signature fonctionnelle est la donnée d'une séquence de …
Colloque
Le défi crucial dans la vérification de l’exactitude des systèmes matériels réside dans le fait que de tels systèmes complexes doivent répondre à des exigences de synchronisation strictes pour assumer en même temps la spécification des performances du produit original, ainsi que les diverses contraintes de l’environnement dans lequel ils sont utilisés. Étant donnée le nombre presque infini et la diversification des vecteurs de tests dont on aurait besoin pour atteindre une couverture des erreurs possibles, d’autre techniques ont vu le jour pour complementer la vérification traditionnelle par simulation. L’une de ces nouvelles techniques très prometteuses est la méthode de …
Colloque
Les circuits logiques n'ont pas cessé d'être de plus en plus complexes. Les techniques classiques de vérification, comme la simulation, se sont avérées incapables d'affronter une telle complexité. De nouvelles techniques de vérification baptisées méthodes formelles ont vu le jour. Ces techniques peuvent impliquer l'utilisation de démonstrateurs de théorèmes ou de vérificateurs d'équivalence. Le principal avantage des démonstrateurs de théorèmes est leur capacité à vérifier des circuits complexes. Cependant, ces outils nécessitent une certaine expertise. D'autre part, ils requièrent une interaction permanente avec l'utilisateur. Les vérificateurs d'équivalence quant à eux sont entièrement autonomes. Cependant, ils échouent à vérifier des circuits …
