Academic literature on the topic 'Vérification RTL'

Cette thèse se situe dans le contexte de la vérification fonctionnelle des circuits intégrés complexes. L’objectif de ce travail est de créer un flot de vérification conjoint au flot de conception basé sur une technique appelée "vérification basée sur les assertions(ABV)". Le concept de base du flot est le raffinement automatique des spécifications formelles données sous la forme d’assertions PSL du niveau TLM au niveau RTL. La principale difficulté est la disparité des deux domaines : au niveau TLM, les communications sont modélisées par des appels de fonctions atomiques. Au niveau RTL, les échanges sont assurés par des signaux binaires évoluant selon un protocole de communication précis. Sur la base d’un ensemble de règles de transformation temporelles formelles, nous avons réalisé un outil permettant d’automatiser le raffinement de ces spécifications. Comme le raffinement des modèles, le raffinement des assertions n’est pas entièrement automatisable : des informations temporelles et structurelles doivent être fournies par l’utilisateur. L’outil réalise la saisie de ces informations de façon ergonomique, puis procède automatiquement à la transformation temporelle et structurelle de l’assertion. Il permet la génération d’assertions RTL mais aussi hybrides. Les travaux antérieurs dans ce domaine sont peu nombreux et les solutions proposées imposent de fortes restrictions sur les assertions considérées. À notre connaissance, le prototype que nous avons mis en oeuvre est le premier outil qui réalise un raffinement temporel fondé sur la sémantique formelle d’un langage de spécification standard (PSL)
The context of this thesis is the functional verification of complex integrated circuits.The objective of our work is to create a seamless verification flow joint to the design flowand based on a proved technique called Assertions-Based Verification (ABV). The mainchallenge of TLM to RTL refinement is the disparity of these two domains : at TLM,communications are modeled as atomic function calls handling all the exchanged data.At RTL, communications are performed by signals according to a specific communicationprotocol. The proposed temporal transformation process is based on a set of formaltransformation rules. We have developed a tool performing the automatic refinement ofPSL specifications. As for design refinement assertion refinement is not fully automated.Temporal and structural information must be provided by the user, using an ergonomicinterface. The tool allows the generation of assertions in RTL but also hybrid assertions.Little work has been done before in this area, and the proposed solutions suffer from severerestrictions. To our knowledge, our prototype is the first tool that performs a temporaltransformation of assertions based on the formal semantics of a standard specificationlanguage (PSL)

Cette thèse introduit un nouveau concept dans la vérification des circuits au niveau RTL : l'interopérabilité entre simulateurs HDL, émulateurs matériel et plateformes de prototypage. Cela permet de bénéficier, à la fois de l'excellente vitesse d'exécution des plateformes de prototypage et des capacités de déboguage, d'observabilité et contrôlabilité offertes par les émulateurs matériel et simulateurs HDL. L'idée principale consiste en la réalisation des tests sur une plateforme de prototypage rapide tout en réalisant périodiquement des sauvegardes de l'état du circuit. Lorsqu'une erreur apparait, le déboguage est réalisé, soit un émulateur rapide, soit un simulateur HDL économique: le test est alors rejoué à partir de la dernière sauvegarde d'état réalisée avant l'instant d'apparition du problème. Enfin, cette thèse présente un flot de prototypage, validé sur un circuit industriel «STM HLS25», permettant d'intégrer l'interopérabilité comme une fonctionnalité du circuit
This thesis defines a new concept in RTL verification: interoperability between HDL simulators, hardware emulators and hardware prototyping platforms. The main purpose is to benefit from both good speed of hardware prototyping platforms and de bug capabilities of hardware emulators and HDL simulators. To achieve this purpose, this thesis introduces the notion of design state. Then, a interoperability dedicated tool is presented. This tool add interoperability to design functionnalities. Thus, ail machines working at RTL level are interoperables with each others. The main idea of interoperability is to lunch tests on fast prototyping platforms while periodically saving design state. When a bug will be faced, debug will be performed using a fast emulator or a low cost HDL simulator. The test will restart from the last database saved just before bug time. Finally, this thesis introduce a new prototyping flow which was validated on an industrial design «STM HLS25»

De nos jours la conception des IP (IP: Intellectual Property) peut bénéficier de nouvelles techniques de vérification symbolique: abstraction de donnée et analyse statique formelle. Nous pensons qu'il est nécessaire de séparer clairement le Contrôle des Données avant toute vérification automatique. Nous avons proposé une définition du contrôle qui repose sur l'idée intuitive qu'il a un impact sur le séquencement de données. Autour de cette idée, le travail a consisté à s'appuyer sur la sémantique des opérateurs booléens et proposer une extension qui exprime cette notion deséquencement. Ceci nous a mené à la conclusion que la séparation parfaite du contrôle et des données est illusoire car les calculs dépendent trop de la représentation syntaxique. Pour atteindre notre objectif, nous nous sommes alors basés sur la connaissance fournie par le concepteur: séparation a priori des entrées contrôle et des entrées données. De cela, nous avons proposé un algorithme de slicing pour partitionner le modèle. Une abstraction fut alors obtenue dans le cas où le contrôle est bien indépendant des données. Pour accélérer les simulations, nous avons remplacé le traitement de données, défini au niveau bit par un modèle d'exécution fonctionnel, tout en gardant inchangé la partie contrôle. Ce modèle intègre des aspects temporels qui permet de se greffer sur des outils de model checking. Nous introduisons la notion de significativité support des données intentionnelles dans les modèles IP. La significativité est utilisée pour représenter des dépendances de données booléennes en vue de vérifier formellement et statiquement les lots de données. Nous proposons plusieurs approximations qui mettent en oeuvre cette nouvelle notion.

Les SVM (Support Vector Machines) sont de nouvelles techniques d'apprentissage statistique proposées par V.Vapnik en 1995. Elles permettent d'aborder des problèmes très divers comme le classement, la régression, la fusion, etc... Depuis leur introduction dans le domaine de la Reconnaissance de Formes (RdF), plusieurs travaux ont pu montrer l'efficacité de ces techniques principalement en traitement d'image. L'idée essentielle des SVM consiste à projeter les données de l'espace d'entrée (appartenant à deux classes différentes) non-linéairement séparables dans un espace de plus grande dimension appelé espace de caractéristiques de façon à ce que les données deviennent linéairement séparables. Dans cet espace, la technique de construction de l'hyperplan optimal est utilisée pour calculer la fonction de classement séparant les deux classes. Dans ce travail de thèse, nous avons étudié les SVM comme techniques de classement pour la Vérification Automatique du Locuteur (VAL) en mode dépendant et indépendant du texte. Nous avons également étudié les SVM pour des tâches de fusion en réalisant des expériences concernant deux types de fusion, la fusion de méthodes et la fusion de modes. Dans le cadre du projet PICASSO, nous avons proposé un système de VAL en mode dépendant du texte utilisant les SVM dans une application de mots de passe publics. Dans ce système, une nouvelle modélisation basée sur la transcription phonétique des mots de passe a été proposée pour construire les vecteurs d'entrée pour notre classifieur SVM. En ce qui concerne notre étude des SVM en VAL en mode indépendant du texte, nous avons proposé des systèmes hybrides GMM-SVM. Dans ces systèmes, trois nouvelles représentations de données ont été proposées permettant de réunir l'efficacité des GMM en modélisation et les performances des SVM en décision. Ce travail entre dans le cadre de nos participations aux évaluations internationales NIST. Dans le cadre du projet BIOMET sur l'authentification biométrique mené par le GET (Groupe des Écoles de Télécommunications), nous avons étudié les SVM pour deux tâches de fusion. La première concerne la fusion de méthodes où nous avons fusionné les scores obtenus par les participants à la tâche ``One Speaker Detection'' aux évaluations NIST'2001. La seconde concerne la fusion de modes menée sur les scores obtenus sur les quatre différentes modalités de la base de données M2VTS. Les études que nous avons réalisées représentent une des premières tentatives d'appliquer les SVM dans le domaine de la VAL. Les résultats obtenus montrent que les SVM sont des techniques très efficaces et surtout très prometteuses que ce soit pour le classement ou la fusion.

La vérification symbolique de systèmes matériels est limitée par la complexité exponentielle en taille de représentation du modèle symbolique sous-jacent.
Ce travail porte sur la réduction, manuelle ou non, de ce modèle. Les approches compositionnelles structurelles et comportementales ont été étudiées dans un contexte industriel. Cette étude a précédé le développement d'une nouvelle technique de réduction : la partition fonctionnelle. Cette technique s'applique aux systèmes dont le comportement est séquentiellement décomposable. La partition fonctionnelle est mise en place grâce à une étape préliminaire de simulation symbolique. Elle a été implémentée et appliquée sur un circuit industriel de taille importante, et a permis d'obtenir d'excellents résultats en matière de réduction. L'expérimentation des techniques de preuve présentées s'est appuyée sur un outil d'extraction de machines d'états finis à partir de descriptions VHDL qu'il a été nécessaire de mettre en œuvre.

Ce travail de thèse introduit un nouveau concept dans la vérification des circuits au niveau RTL : l'interopérabilité entre simulateurs HDL, émulateurs matériel et plateformes de prototypage. Cela permet de bénéficier, à la fois de l'excellente vitesse d'exécution des plateformes de prototypage et des capacités de déboguage, d'observabilité et contrôlabilité offertes par les émulateurs matériel et simulateurs HDL. L'idée principale de l'interopérabilité consiste en la réalisation des tests sur une plateforme de prototypage rapide tout en réalisant périodiquement des sauvegardes de l'état du circuit. Lorsqu'une erreur apparait, le déboguage est réalisé, soit un émulateur rapide, soit un simulateur HDL économique : le test est alors rejoué à partir de la dernière sauvegarde d'état réalisée avant l'instant d'apparition du problème. Enfin, cette thèse présente un flot de prototypage, validé sur un circuit industriel STM HLS25, permettant d'intégrer l'interopérabilité comme une fonctionnalité du circuit