| Titre : | Techniques Formelles pour la Preuve d'Equivalence de Circuits Séquentiels | | Type de document : | texte imprimé | | Auteurs : | S. RAHIM, Auteur | | Année de publication : | 2004 | | Langues : | Français (fre) | | Tags : | PREUVE D'EQUIVALENCE IMPLANTATION SPECIFICATION SYNTHESE BDDS AIGS POINT D'EQUIVALENCE PARCOURS DES ETATS RELATION DE CORRESPONDANCE (RC) BASCULES OPTIMISATIONS SEQUENTIELLES A SEQUENTIAL EQUIVALENCE CHECKING TOOL FOR OPTIMIZED CIRCUITS EQUIVALENCE CHECKING BDDS AIGS STATE TRAVERSAL RC SUBSPACE | | Index. décimale : | THE Thèses de doctorat | | Résumé : | Les techniques de preuve d'équivalence permettent de vérifier que la fonctionnalité d'un circuit ne change pas après une étape de la phase de conception. Ces techniques sont souvent utilisées pour vérifier que l'implantation obtenue après synthèse est fonctionnellement équivalente au circuit de départ. La méthode générale pour la vérification fonctionnelle de circuits séquentiels appelée aussi méthode de parcours des états n'est pas applicable pour des circuits de grande taille. Pour résoudre ce problème, les outils industriels de preuve d'équivalence essayent souvent de transformer le problème de la vérification de circuits séquentiels en un problème de vérification de circuits combinatoires. Pour cela, ils calculent une relation de correspondance (RC) entre les bascules de l'implantation et de la spécification. Cette relation permet d'identifier entre les deux circuits des bascules qui potentiellement ont des fonctions d'entrées équivalentes. L'entrée de ces bascules est ensuite transformée en sortie primaire et leur sortie en entrée primaire. Cette transformation permet de migrer le problème d'équivalence de circuits séquentiels en un problème d'équivalence combinatoire. Malheureusement les méthodes utilisées par les outils de vérification industriels pour le calcul de la RC ne permettent pas de prendre correctement en considération les optimisations séquentielles effectuées par l'outil de synthèse. Nous proposons dans ce mémoire un flot de vérification permettant de vérifier des circuits industriels optimisés séquentiellement. L'efficacité de notre flot provient de notre méthode de construction de la RC. L'utilisation d'une technique brevetée dite de Subspace dans ce calcul nous permet de prendre en compte des optimisations séquentielles complexes comme les fusions, les réplications et l'élimination de bascules redondantes. Un autre avantage de notre flot de vérification est sa capacité à vérifier des circuits qui ont subi des optimisations sur les délais. Finalement, nous montrons l'efficacité de notre flot de vérification en l'appliquant sur des circuits industriels de grande taille.
Equivalence checking is the process of checking if two given designs have the same functionality, e.g. an optimized design is functionally equivalent to its earlier version. This is often used to verify if the synthesized circuit, which is also called implementation is functionally equivalent to the departure circuit, which is also called specification. General algorithms for sequential equivalence checking are computationally expensive because they require a state space traversal. This is the main reason why commercial tools often use combinational equivalence checking techniques to verify sequential designs. This approach consists in identifying potential equivalent flip-flops or nets in the two designs under verification. This is called the matching step. Then it is needed to verify the equivalence of the corresponding combinational blocks resulting of the matching using combinational formal techniques Due to sequential optimizations performed during synthesis, which can remove, merge, replicate or retime flip-flops, this matching step can be very complex and incomplete. This is why we present a sequential equivalence checking flow, which is able to deal with sequential optimizations, performed by the synthesis tool. The efficiency of our method is due to our matching step. The use of a technique called Subspace makes our matching more efficient to check sequential optimized circuits than the ones computed by the other equivalence checking tools. Moreover our verification flow is also able to verify optimization as retiming. The efficiency of the proposed verification flow is confirmed by experimental results on retimed and optimized industrial circuits. | | Directeur(s) de thèse : | ROUZEYRE B. | | Président du jury : | CIESIELSKI J. | | Rapporteur(s) : | BORRIONE D. | | Examinateur(s) : | BERTHET C.;RAMPON J.;TORRES L. | | Date de soutenance : | 05/07/2004 |
Techniques Formelles pour la Preuve d'Equivalence de Circuits Séquentiels [texte imprimé] / S. RAHIM, Auteur . - 2004. Langues : Français ( fre) | Tags : | PREUVE D'EQUIVALENCE IMPLANTATION SPECIFICATION SYNTHESE BDDS AIGS POINT D'EQUIVALENCE PARCOURS DES ETATS RELATION DE CORRESPONDANCE (RC) BASCULES OPTIMISATIONS SEQUENTIELLES A SEQUENTIAL EQUIVALENCE CHECKING TOOL FOR OPTIMIZED CIRCUITS EQUIVALENCE CHECKING BDDS AIGS STATE TRAVERSAL RC SUBSPACE | | Index. décimale : | THE Thèses de doctorat | | Résumé : | Les techniques de preuve d'équivalence permettent de vérifier que la fonctionnalité d'un circuit ne change pas après une étape de la phase de conception. Ces techniques sont souvent utilisées pour vérifier que l'implantation obtenue après synthèse est fonctionnellement équivalente au circuit de départ. La méthode générale pour la vérification fonctionnelle de circuits séquentiels appelée aussi méthode de parcours des états n'est pas applicable pour des circuits de grande taille. Pour résoudre ce problème, les outils industriels de preuve d'équivalence essayent souvent de transformer le problème de la vérification de circuits séquentiels en un problème de vérification de circuits combinatoires. Pour cela, ils calculent une relation de correspondance (RC) entre les bascules de l'implantation et de la spécification. Cette relation permet d'identifier entre les deux circuits des bascules qui potentiellement ont des fonctions d'entrées équivalentes. L'entrée de ces bascules est ensuite transformée en sortie primaire et leur sortie en entrée primaire. Cette transformation permet de migrer le problème d'équivalence de circuits séquentiels en un problème d'équivalence combinatoire. Malheureusement les méthodes utilisées par les outils de vérification industriels pour le calcul de la RC ne permettent pas de prendre correctement en considération les optimisations séquentielles effectuées par l'outil de synthèse. Nous proposons dans ce mémoire un flot de vérification permettant de vérifier des circuits industriels optimisés séquentiellement. L'efficacité de notre flot provient de notre méthode de construction de la RC. L'utilisation d'une technique brevetée dite de Subspace dans ce calcul nous permet de prendre en compte des optimisations séquentielles complexes comme les fusions, les réplications et l'élimination de bascules redondantes. Un autre avantage de notre flot de vérification est sa capacité à vérifier des circuits qui ont subi des optimisations sur les délais. Finalement, nous montrons l'efficacité de notre flot de vérification en l'appliquant sur des circuits industriels de grande taille.
Equivalence checking is the process of checking if two given designs have the same functionality, e.g. an optimized design is functionally equivalent to its earlier version. This is often used to verify if the synthesized circuit, which is also called implementation is functionally equivalent to the departure circuit, which is also called specification. General algorithms for sequential equivalence checking are computationally expensive because they require a state space traversal. This is the main reason why commercial tools often use combinational equivalence checking techniques to verify sequential designs. This approach consists in identifying potential equivalent flip-flops or nets in the two designs under verification. This is called the matching step. Then it is needed to verify the equivalence of the corresponding combinational blocks resulting of the matching using combinational formal techniques Due to sequential optimizations performed during synthesis, which can remove, merge, replicate or retime flip-flops, this matching step can be very complex and incomplete. This is why we present a sequential equivalence checking flow, which is able to deal with sequential optimizations, performed by the synthesis tool. The efficiency of our method is due to our matching step. The use of a technique called Subspace makes our matching more efficient to check sequential optimized circuits than the ones computed by the other equivalence checking tools. Moreover our verification flow is also able to verify optimization as retiming. The efficiency of the proposed verification flow is confirmed by experimental results on retimed and optimized industrial circuits. | | Directeur(s) de thèse : | ROUZEYRE B. | | Président du jury : | CIESIELSKI J. | | Rapporteur(s) : | BORRIONE D. | | Examinateur(s) : | BERTHET C.;RAMPON J.;TORRES L. | | Date de soutenance : | 05/07/2004 |
|
Affiner la recherche Interroger des sources externesTechniques Formelles pour la Preuve d'Equivalence de Circuits Séquentiels / S. RAHIM
