Brevet FR3000255A1 — publié le 20140627

B11702 1 PROCÉDÉ ET DISPOSITIF DE VÉRIFICATION D'ÉQUIVALENCE Domaine La présente description concerne un procédé et un dispositif pour vérifier que deux représentations de circuit sont fonctionnellement équivalentes. Arrière-plan La figure 1 illustre un exemple d'un procédé typique de conception de circuit intégré. Comme cela est représenté à gauche de la figure 1, initialement le processus de conception implique par exemple une implémentation architecturale 101 du circuit. Une implémentation RTL (niveau de transfert en registres) 102 est alors par exemple développée, suivie d'une implémentation de circuit 103 et d'une implémentation topologique 104. Comme cela est représenté à droite de la figure 1, pendant l'implémentation de circuit 103, une spécification RTL 103A est par exemple traitée en utilisant une synthèse à partir de cellules pour produire une implémentation en cellules standard 103B. Par exemple, la représentation de circuit est transformée à partir de la spécification RTL en une implémenta- tion en cellules standard utilisant des cellules standard choisies dans une bibliothèque de cellules. Des modifications techniques sont alors par exemple appliquées à l'implémentation B11702 2 en cellules standard 103B, par exemple pour amener la représentation de circuit en conformité avec certaines contraintes de conception telles que la vitesse du circuit, en d'autres termes des retards de propagation, ainsi que par exemple la consomma- tion ou la dimension de puces, pour produire l'implémentation finale 103C. A diverses phases du processus de conception, on réalise une vérification pour vérifier que la dernière représentation est fonctionnellement équivalente à une ou plusieurs représentations précédentes et en particulier qu'aucun défaut n'a été introduit dans la fonctionnalité de la représentation. Une telle vérification est généralement appelée vérification d'équivalence. Par exemple, on peut vérifier que l'implémentation en cellules standard 103E est fonctionnellement équivalente à la spécification RTL 103A et/ou que l'implémentation finale 103C est fonctionnellement équivalente à l'implémentation en cellules standard 103B. Les représentations de circuit modernes sont généralement extrêmement complexes et ainsi des techniques particulières 20 ont été développées pour réaliser ce type de vérification d'équivalence. Ces techniques impliquent généralement l'une ou l'autre de deux approches. Selon une première approche, la fonctionnalité du circuit est comparée en élaborant un circuit unique de vérification d'équivalence, généralement désigné dans 25 la technique par l'appellation circuit "miter", et en vérifiant ensuite que les sorties primaires des circuits sont fonctionnellement équivalentes pour tout l'ensemble d'états possibles. Selon une seconde approche, des registres qui se correspondent dans les conceptions sont identifiés en tant que points de 30 coupure, et on tente de prouver que les fonctions d'entrée booléennes de ces registres circuits sont équivalentes. La seconde approche, est relativement restrictive 35 auxquels elle peut s'appliquer et les sorties primaires des basée sur les circuits accordés, qüànt aux types de circuits en raison d'un manque d'optimisa- B11702 3 tion séquentielle et est souvent peu fiable. Toutefois, la première approche basée sur un circuit "miter" est rendue difficile par le besoin de vérifier que tous les états possibles de la présentation de circuit ont été introduits pendant la vérification. Pour cela, il est habituellement nécessaire de connaître le nombre d'états atteignables de la représentation de circuit. Des solutions existantes pour déterminer le nombre d'états atteignables de la représentation de circuit impliquent la réalisation d'une décomposition de la représentation de circuit. Toutefois, pour des représentations de circuit de relativement forte complexité, ces solutions sont généralement très lentes à mettre en oeuvre et/ou sont limitées par la complexité de la conception. En outre, dans certains cas, l'exécution peut être limitée par les ressources de calcul disponibles, par exemple en termes de mémoire vive (RAM). Il y a donc un problème technique pour prévoir un procédé et un dispositif pour vérifier, de façon relativement simple et efficace temporellement, si deux représentations de circuit sont fonctionnellement équivalentes. Résumé Un objet de modes de réalisation de la présente invention est de traiter au moins partiellement un ou plusieurs besoins de l'état de la technique. Selon un aspect, il est prévu un procédé de vérification par un dispositif de traitement de ce que des première et seconde représentations de circuit sont fonctionnellement équivalentes comprenant : déterminer un nombre minimum de transitions d'états de la première représentation de circuit pour atteindre tous ses états en : calculant par le dispositif de traitement pour chaque première et seconde itérations successives d'au moins une partie de la première représentation de circuit, une première fonction caractéristique associée à un premier groupe de r registres et sur la base d'un nombre mvar de variables d'entrée, où r et mvar sont des entiers - supérieur ou égal à 1, r étant inférieur au nombre total de B11702 4 registres dans la première représentation de circuit, et/ou mvar étant inférieur au nombre total d'entrées de la première représentation de circuit ; comparant les premières fonctions caractéristiques calculées pour le premier groupe de registres 5 pour les première et seconde itérations successives; et si les premières fonctions caractéristiques concordent, déterminant le nombre minimal de transitions d'états sur la base du nombre d'itérations réalisées jusqu'à la seconde itération et comparer les sorties des première et seconde représentations de 10 circuit pour le nombre minimal de transitions d'états. Selon un mode de réalisation, la première fonction caractéristique est calculée pour le premier groupe de r registres et une seconde fonction caractéristique est calculée pour au moins un second groupe de r registres. 15 Selon un mode de réalisation, la détermination d'un nombre minimal de transitions d'états de la première représentation de circuit comprend en outre un second appel des étapes a) à c) sur la base de la seconde fonction caractéristique associée à un autre groupe de r' registres, r' 20 étant un entier avec rv>r. Selon un mode de réalisation, r est un nombre premier. Selon un mode de réalisation, l'étape a) est réalisée pour x groupes de registres, x étant égal à la partie entière par excès de (N/r), N étant le nombre total de registres. 25 Selon un mode de réalisation, la première fonction caractéristique est produite sur la base d'une substitution d'au moins une valeur d'entrée de la représentation de circuit par une valeur fixée. Selon un mode de réalisation, la valeur d'entrée est 30 fixée à une valeur déterminée et/ou à la valeur d'une autre valeur d'entrée du circuit. Selon un mode de réalisation, chaque itération de la partie de la première représentation de circuit comprend une duplication des entrées et le placement des fonctions d'entrée 35 de chacun des registres à leurs sorties. B11702 Selon un mode de réalisation, il est prévu un dispositif de traitement adapté à la mise en oeuvre du priocédé ci-dessus. Selon un autre aspect, il est prévu Dispositif de 5 traitement agencé pour vérifier si des première et seconde représentations de circuit sont fonctionnellement équivalentes, le dispositif de traitement étant agencé pour : déterminer un nombre minimum de transitions d'états de la première représentation de circuit pour atteindre tous ses états en : calculant par le dispositif de traitement pour chaque première et seconde itérations successives d'au moins une partie de la première représentation de circuit, une première fonction caractéristique associée à un premier groupe de r registres et sur la base d'un nombre mvar de variables d'entrée, où r et mvar sont des entiers supérieur ou égal à 1, r étant inférieur au nombre total de registres dans la première représentation de circuit, et mvar étant inférieur au nombre total d'entrées de la première représentation de circuit ; comparant les premières fonctions caractéristiques calculées pour le premier groupe de registres pour les première et seconde itérations successives; et si les premières fonctions caractéristiques concordent, déterminant le nombre minimal de transitions d'états sur la base du nombre d'itérations réalisées jusqu'à la seconde itération ; et comparer les sorties des première et seconde représentations 25 de circuit pour le nombre minimal de transitions d'états. Selon un mode de réalisation, il est prévu un dispositif de mémorisation lisible par ordinateur mémorisant un programme d'ordinateur comprenant des instructions qui, quand elles sont exécutées par un ordinateur, amènent le procédé ci- 30 dessus à être mis en oeuvre. Brève description des figures Ces buts, caractéristiques, aspects et avantages de l'invention ainsi que d'autres apparaîtront à la lecture de la description détaillée suivante de modes de réalisation faite à B11702 6 titre illustratif et non-limitatif en relation avec les dessins joints parmi lesquels : la figure 1, décrite précédemment, illustre schématiquement un exemple d'étapes d'un processus de conception typique 5 d'un circuit intégré ; la figure 2 représente schématiquement un circuit propre à vérifier si deux représentations de circuit sont fonctionnement équivalentes ; la figure 3 est un organigramme illustrant des étapes 10 de ce que deux représentations de d'un procédé de vérification circuit sont fonctionnellement équivalentes, selon un exemple de réalisation ; la figure 4 est un diagramme d'état représentant un exemple des états d'une représentation de circuit ; 15 la figure 5 est un organigramme illustrant des étapes d'un procédé de détermination d'un nombre d'états possibles dans une représentation de circuit selon un exemple de réalisation ; la figure 6A représente schématiquement un exemple de réalisation de la représentation de circuit de la figure 2 ; 20 La figure 6B représente plus en détail une représenta- tion de circuit selon un exemple de réalisation ; et la figure 7 représente un dispositif électronique pour mettre en oeuvre les procédés des figures 3 et 5, selon un exemple de réalisation. 25 Description détaillée de modes de réalisation La figure 2 représente schématiquement un circuit 200 de vérification de ce qu'une représentation de circuit 201 est fonctionnellement équivalente à une représentation de circuit 202. Un tel circuit est couramment appelé circuit "miter". La 30 représentation de circuit 201 correspond par exemple à une mise en oeuvre sous forme de cellules standard ou à une réalisation finale, telles que celles désignées par 103B et 1030 en figure 1, et la représentation de circuit 202 correspond par exemple à une spécification RTL telle que celle désignée par 103A en 35 figure 1. A titre de variante, la représentation de circuit 201 B11702 7 et/ou 202 pourrait correspondre à des représentations produites à d'autres étape du processus de conception. Chacune des représentations de circuit 201, 202 comprend par exemple des blocs logiques combinatoires 204, 204' 5 respectivement et des blocs logiques séquentiels 205, 205' respectivement. Le bloc logique séquentiel 205 reçoit par exemple la sortie du bloc logique combinatoire 204 et produit une sortie vers le bloc 204. De façon similaire, le bloc logique séquentiel 205' reçoit par exemple la sortie du bloc logique 10 combinatoire 204' et produit une sortie vers le bloc 204'. Les blocs logiques combinatoires 204, 204' et/ou les blocs logiques séquentiels 205, 205' peuvent correspondre à des représentations de circuit complètes 201, 202 ou à une partie de ces représenta- tions de circuit. 15 Les entrées primaires respectives 206, 206' des blocs logiques combinatoires 204, 204' sont confondues. Les sorties primaires respectives 208, 208' des blocs logiques combinatoires 204 et 204' sont couplées aux entrées correspondantes d'une porte OU-Exclusif, XOR, 210. Dans des variantes de réalisation, 20 la porte OU-Exclusif 210 pourrait être remplacée par une porte NON OU-Exclusif (XNOR). Les lignes de données d'entrée sont alors affectées de certaines valeurs d'entrée lors d'itérations successives du circuit et la séquence de sortie correspondante est vérifiée 25 pour assurer que la valeur R à la sortie de la porte OU-Exclusif 210 reste basse, impliquant que les valeurs de chacun des circuits 201, 202 concordent. La figure 3 est un organigramme illustrant des étapes d'un procédé de vérification de l'équivalence entre les repré30 sentations de circuit sur la base du circuit "miter" de la figure 2, selon un exemple de réalisation. Un tel procédé est par exemple mis en oeuvre par un dispositif de traitement. Lors d'une première étape 301, le circuit "miter" est élaboré sur la base des deux représentations de circuit. En 35 particulier, les circuits à comparer sont par exemple en format B11702 8 RTL et peuvent être transformés en représentation AIG (graphe des portes ET/Inverseurs), ou analogue. Cette étape implique par exemple la lecture des représentations de circuit et la mise en concordance des entrées équivalentes de chaque circuit. En outre, les sorties des circuits sont combinées par exemple en utilisant une porte XOR ou XNOR. Lors d'une étape ultérieure 302, plusieurs états atteignables des représentations de circuit sont déterminés. Comme cela sera décrit plus en détail ci-après, ceci implique un calcul simplifié dans lequel le nombre de registres considérés à la fois et/ou le nombre de variables d'entrée est réduit. Lors d'une étape ultérieure 303, les sorties primaires de chacune des représentations de circuit sont comparées pour tous les états atteignables. En particulier, les sorties primaires sont comparées lors d'itérations successives de la représentation de circuit en supposant certaines valeurs de données d'entrée à chaque itération et en calculant les valeurs de sortie correspondantes. Le nombre d'itérations est basé sur le nombre d'états atteignables déterminé à l'étape 302. Lors d'une étape ultérieure 304, on détermine si des erreurs sont détectées entre les sorties primaires des représentations de circuit 201, 202 pour chacune des itérations des circuits. Si oui, à une étape 305, un message d'erreur est par exemple affiché sur un affichage couplé au dispositif de traite-25 ment mettant en oeuvre le procédé. Si par contre il n'y a pas d'erreur, l'étape suivante est l'étape 306 au cours de laquelle on considère que les représentations sont fonctionnellement équivalentes et un message correspondant est par exemple affiché sur l'affichage. 30 L'homme de l'art notera que, bien que les étapes 302 à 306 de la figure 3 soient illustrées et décrites ci-dessus comme des étapes séquentielles, dans des variantes de réalisation, la comparaison des sorties primaires des représentations de circuit pourrait être réalisée à chaque itération de la représentation B11702 9 de circuit en parallèle avec la détermination du nombre d'états atteignables. La figure 4 est un diagramme d'état correspondant à un exemple d'une partie relativement simple d'une représentation de circuit. Dans cet exemple, il y a un total de 6 états SO à S5. De façon générale, tout circuit logique comportant un ou plusieurs registres synchrones peut être considéré comme une machine d'état, les états étant indiqués par les valeurs des registres, et les transitions entre états étant déterminées par 10 les valeurs de registre précédentes et/ou par les données d'entrée. Par exemple, la logique représentée par le diagramme d'état de la figure 4 comprend trois registres à 1 bit et les états SO à S5 correspondent respectivement aux valeurs "000" 15 "010", "011", "100", "001" et "101" mémorisées par ces registres. Les flèches entre les états de la figure 4 indiquent des transitions d'états qui peuvent survenir à chaque itération des représentations de circuit, en d'autres termes, lors de 20 chaque nouveau cycle d'horloge. Ainsi, pendant cinq itérations initiales des états de la représentation de circuit, en partant de l'état SO, les états atteignables sont les suivants : 0 SO 1 SO S1 S5 25 2 SO S1 S2 S5 3 SO S1 S2 S3 S5 4 SO S1 S2 S3 S4 S5 SO S1 S2 S3 S4 S5 Les états indiqués en gras dans cette liste correspondent aux 30 nouveaux états qui peuvent être atteints à chaque nouvelle itération. Après la quatrième itération de la représentation de circuit, les six états atteignables ont été atteints et ainsi aucun nouvel état n'est trouvé lors de la cinquième itération. Ainsi, si pour deux itérations successives le nombre d'états B11702 10 atteignables reste le même, -ceci implique que tous les états atteignables ont été trouvés. La figure 5 est un organigramme illustrant des étapes dans un procédé de mise en oeuvre de l'étape 302 de la figure 3, en d'autres termes pour déterminer le nombre d'états atteignables dans une représentation de circuit, et plus particulièrement un nombre minimum d'itérations pour tous les états de la représentation de circuit à atteindre. Le procédé de la figure 5 fournit par exemple une valeur qui est une estimation très fiable du nombre vrai d'états atteignables dans la représentation de circuit. Dans de nombreux cas, cette valeur est suffi-samment fiable pour être utilisée directement dans l'opération de vérification d'équivalence. A titre de variante, il sera clair pour l'homme de l'art que des techniques pourraient être utilisées pour confirmer la valeur obtenue. Lors d'une première étape 501, un état initial de la représentation de circuit 201 est établi automatiquement par le système ou par un utilisateur. Cette étape va maintenant être expliquée plus en détail avec les figures EA et 6B. La figure 6A représente schématiquement un exemple des représentations de circuit 201 et 202. Chacune des représenta- tions de circuit 201, 202 comprend des registres dont six registres R1 à R6 de la représentation de circuit 201 et six registres R1' à R6' de la représentation de circuit 202 sont 25 représentés. Chacun des registres R1 à R6 mémorise par exemple un bit de données. Plusieurs lignes d'entrée 206, 206' et des lignes de sortie 208, 208' de chacune des représentations de circuit 201, 202 sont également représentées. Par souci de clarté, aucun circuit intermédiaire interconnectant les divers 30 registres n'est représenté en figure 6A. Les valeurs mémorisées par les registres des représentations de circuit 201, 202 déterminent leurs états. L'état initial de chacune des représentations de circuit correspond par exemple à un zéro logique mémorisé par chacun des registres. A 35 titre de variante, chaque valeur de bit pourrait être B11702 11 initialisée à l'une des trois valeurs : '0' logique, '1' logique ou '-' pour inconnu et il y a donc de nombreux états différents qui pourraient être établis en tant qu'état initial. L'étape 501 de la figure 5 implique par exemple l'ini- tialisation des registres de cette manière. A titre de variante, un état initial des registres pourrait être fourni par un utilisateur. La figure 6B représente un exemple plus détaillé d'un circuit "miter" construit à partir des représentations de 10 circuit 201 et 202. Dans cet exemple, la représentation de circuit 201 comprend des lignes d'entrée a et b dont chacune est couplée par l'intermédiaire d'un inverseur correspondant 602 à une entrée correspondante d'une porte ET 604. La sortie de la porte ET 604 15 est couplée à un registre Ri. La sortie du registre R1 est couplée par un autre inverseur 606 à une entrée d'une porte ET 608, sa seconde entrée étant couplée à une ligne d'entrée c de la représentation de circuit 201. La représentation de circuit 202 est par exemple iden20 tique à la représentation de circuit 201 sauf que les inverseurs 602 et 606 sont supprimés et que la porte ET 604 est remplacée par une porte OU 610. Dans l'exemple de la figure 6B, les données mémorisées par les registres R1 et R1' déterminent les états des circuits. 25 Toutefois, dans cet exemple, les registres R1 et R1' sont par exemple initialisés à des valeurs opposées car, autrement, en raison de l'inverseur 606, on trouverait que les fonctions de sortie primaires des représentations de circuit diffèrent lors de la première itération alors que, en fait, les représentations 30 de circuit 201 et 202 de la figure 6E sont fonctionnellement équivalentes. En se référant à nouveau de la figure 5, à l'étape 501, une variable i représentant un nombre d'itérations de la représentation de circuit est par exemple initialisée à 0. B11702 12 Lors d'une étape suivante 502, un paramètre x est établi à une valeur égale au nombre total N de registres divisé par un paramètre r. En particulier, comme cela sera décrit plus en détail ci-après, pendant un processus itératif de recherche 5 d'un point fixe auquel aucun nouvel état du circuit n'est atteint, les registres sont par exemple divisés en groupes. Le paramètre r indique le nombre de registres dans chaque groupe. Le paramètre r est par exemple inférieur au nombre total de registres dans chaque représentation de circuit, bien 10 que, dans certains cas, le paramètre r puisse être supérieur ou égal au nombre total de registres, auxquels cas tous les registres seraient considérés à la fois. Dans certains modes de réalisation, le paramètre r pourrait être sélectionné de façon aléatoire. 15 Dans un autre exemple, le paramètre r est initialement fixé comme étant égal à trois, ce qui correspond à l'exemple de la figure 6A, dans laquelle un groupe des trois premiers registres R1, R2 et R3 est considéré initialement. Si le nombre total N de registres n'est pas un 20 multiple du paramètre r, la valeur x est par exemple arrondie à la valeur entière immédiatement supérieure. Ainsi, x peut être défini de façon plus générale comme étant égal à la partie entière par excès de (N/r), "ceiling(N/r)". En ce cas, la dimension du groupe final de registres est adaptée en conséquence. 25 Par exemple, la représentation de circuit 201 de la figure 6A peut comprendre un total de 10 registres R1 à R10 avec r égal à 3, le paramètre x est égal à 4, les groupes comprenant un premier groupe 600 de registres R1 à R3, un second groupe 601 de registres R4 à R6, un troisième groupe de registres R7 à R9, 30 (nom représenté en figure 6A,) et un quatrième groupe comprenant un registre R10 (également non représenté en figure 6A). De façon similaire, la représentation de circuit 202 de la figure 6A peut comprendre un total de 10 registres R1 à R10 comprenant un premier groupe 600' de registres R1' à R3', un deuxième 35 groupe 601' de registres R4' à R6', un troisième groupe de B11702 13 registres R7' à R9' (non représenté en figure 6A) et un quatrième groupe consistant en un registre R101 (également non représenté en figure 6A). Egalement, à l'étape 502, les fonctions caractéris5 tiques CF1 à CFx sont initialisées, par exemple à zéro. Ces fonctions caractéristiques CF' à CFx représentent respectivement une fonction caractéristique des x groupes de registres du circuit "miter" comme cela sera décrit plus en détail ci-après. A une étape ultérieure 503, les fonctions d'entrée des 10 registres pour chacun des registres sont calculées dans le domaine générique sur la base d'un nombre "mvar" de variables d'entrée. Par exemple, sur la base d'une représentation Sous forme standard de la représentation de circuit, telle qu'une représentation BDD (diagramme de décision binaire) ou AIG 15 (graphe des portes ET/Inverseurs), la relation entre chaque valeur de registre et les valeurs de données d'entrée peut être déterminée pour toutes les variables d'entrée primaires. Pour des représentations de circuit relativement complexes et/ou des nombres élevés de registres, il peut être préférable d'utiliser 20 la représentation AIG. Les fonctions d'entrée de registres sont par exemple mémorisées pour être utilisées lors d'une itération ultérieure. Par exemple, dans l'exemple de la figure 6B, la fonction d'entrée du registre R1 est par exemple calculée comme 25 étant FR' = ai), alors que la fonction d'entrée pour le registre R1' est par exemple calculée comme étant FR1'= a + b. Les fonctions d'entrée de registre sont alors par exemple réduites sur la base de la valeur de mvar, qui indique le nombre de variables d'entrée. Par exemple, dans cette étape, 30 les variables d'entrée du circuit sont limitées à un nombre mvar, sur la base d'une technique de simulation symbolique. Par exemple, une ou plusieurs des lignes d'entrée 206 de la figure 6A sont liées à une valeur logique "1" ou "0" et/ou deux ou plusieurs des lignes d'entrée 206 sont liées ensemble. Ainsi, en 35 supposant un nombre total de n lignes d'entrées, plutôt qu'il y B11702 14 ait un total de 2n valeurs d'entrée différentes qui pourraient être appliquées à chaque itération, le nombre est limité à 2mvar. Par exemple, mvar est choisi égal à un nombre premier. Réduire le nombre de variables d'entrée est une étape optionnelle. En fait, dans certains cas, la variable mvar est égale ou supérieure au nombre de variables d'entrée auquel cas aucune simulation symbolique n'est appliquée. A une étape ultérieure 504, une valeur de point fixe FP est rendue égale à VRAI (TRUE) et une variable j est mise égale à 1. A une étape ultérieure 505, pour le jème groupe de r registres, la fonction mise en oeuvre par ces registres est extraite des fonctions d'entrée de registres pour tous les registres, et la fonction caractéristique CF] correspondant à ce 15 groupe de registres pour l'itération i est déterminée. La fonction caractéristique est un concept bien connu dans le domaine de l'automatisation électronique de la conception.pourciéterminerue CF] ,une technique d'évaluation symbolique de trajectoire (STE - Symbolic 20 Trajectory Evaluation) est par exemple utilisée. En particulier, la fonction caractéristique des registres à un instant t fournit le nombre total d'états accessibles du circuit depuis un instant initial. En considérant le circuit de la figure 6E à titre 25 d'exemple, et en supposant que les variables a et b sont initialement égales à ao et bo, respectivement, à un instant to, ceci donne les valeurs rlo à la sortie du registre R1 et rl'o à la sortie du registre R1' comme suit : rlo = ao.bo 30 rl'o = ao + 130 Ainsi, la fonction caractéristique CF pour les états des registres à l'instant to peut être déterminée comme étant CF = rlo.rro + rlo.rl'o, en d'autres termes, les états possibles sont rlo haut et rro bas, ou inversement. B11702 15 A une étape ultérieure 506, la fonction caractéristique CFj est comparée à une valeur précédemment mémorisée de la fonction caractéristique CF. Lors de la première itération de la boucle, la valeur CF1 reste à sa valeur initialisée car il n'y a pas de fonction caractéristique précédemment mémorisée pour le premier groupe de registres et ensuite l'étape suivante est l'étape 507 à laquelle le paramètre FP est mis égal à FAUX (FALSE) et la nouvelle fonction caractéristique CF1 est mémorisée. Après l'étape 507 ou après l'étape 506 si la fonction caractéristique CFj .concorde, l'étape suivante est l'étape 508 à laquelle on détermine si la variable j est égale au paramètre x. Sinon, l'étape suivante est l'étape 509 à laquelle la variable j est incrémentée et ensuite on revient à l'étape 505 et les étapes 505 à 508 sont répétées pour le jème groupe suivant de registres. Une fois que la variable j est égale à x, en d'autres termes que tous les registres ont été traités, l'étape qui suit après l'étape 508 est l'étape 510. A l'étape 510, on détermine si la boucle courante est 20 un premier ou un second appel du procédé. S'il s'agit d'un premier appel, l'étape suivante est l'étape 511 à laquelle on détermine si la variable FP est encore égale à VRAI. Sinon, l'étape suivante est l'étape 512 au cours de laquelle une transition d'état survient en incrémentant la variable i, et le 25 procédé revient à l'étape 503 comme un nouveau premier appel du procédé. Après un certain nombre de transistions d'état, on atteint un stade auquel les fonctions caractéristiques CF1 à CFx restent constantes d'une itération à la suivante. En 30 particulier, comme cela a été exposé ci-dessus en relation avec le diagramme d'état de la figure 4, l'absence de nouveaux états entre des transitions d'états successives indique que tous les états atteignables de la machine d'état ont été trouvés. Ceci indique qu'il n'y a plus de nouveaux états introduits. Ainsi, à 35 l'étape 511, on détermine que FP est encore mis à VRAI. B11702 16 L'étape suivante après l'étape 511, si le paramètre FP est VRAI est par exemple l'étape 513 à laquelle un second appel du procédé est réalisé avec une nouvelle valeur du paramètre r et/ou du paramètre mvar, et on revient à l'étape 502. Par exemple, si pendant le premier appel le paramètre r est par exemple mis à 3, lors du second appel, ce paramètre est par exemple mis à 5. Dans un mode de réalisation, dans le premier appel du procédé et dans les appels suivantes, un nombre premier est choisi pour la valeur r ce qui a l'avantage d'assurer un nombre relativement faible de frontières communes entre les groupes de registres d'un appel au suivant. Avant de mettre en oeuvre cet second appel, la valeur i est par exemple décrémentée de sorte que les fonctions caractéristiques pour les itérations i et i-1 sont comparées. Si, pendant l'étape 510, on détermine que la boucle courante est un second appel du procédé, l'étape suivante est l'étape 514 au cours de laquelle on détermine si la variable FP est encore égale à VRAI ou non. Si non, l'étape suivante est l'étape 512 au cours de laquelle une transition d'état survient en incrémentant la variable i et on revient à l'étape 503 pour répéter une premier appel du procédé, comme cela a été décrit ci-dessus, sur la base de la nouvelle itération i. A titre de variante, si à l'étape 514 on détermine que la variable FP est VRAI, l'étape suivante est l'étape 515 au cours de laquelle on détermine qu'un point fixe a été atteint. Le résultat indiquant le nombre minimal de transitions d'états est basé sur la valeur i. En particulier, la valeur de la variable i devient par exemple le résultat, indiquant le nombre de transitions d'états jusqu'à la concordance des fonctions caractéristiques. A titre de variante, dans certains modes de réalisation, le résultat pourrait être fixé à i-l. A titre de variante de l'organigramme décrit en relation avec la figure 5, on pourrait sauter directement à l'étape 510 si à l'étape 506 on trouve que la fonction caractéristique 35 CFj ne concorde pas avec la fonction caractéristique CE) précé- B11702 17 demment mémorisée. En fait, ceci indique immédiatement que le point fixe n'a pas encore été atteint. Toutefois, en ce cas, il peut exister d'autres groupes de registres non encore traités par l'itération courante, et les fonctions caractéristiques manquantes de ces groupes de registres sont par exemple calculées lors d'une itération ultérieure. Après l'étape 515, une vérification de la fonction de sortie primaire du circuit "miter" pour tous les états atteignables est par exemple réalisée à l'étape 303 de la figure 3 sur la base du nombre d'états atteignables correspondant au point fixe FP. Par exemple, en prenant l'exemple de la figure 6B, on suppose que, lors de la seconde itération, on a trouvé que la fonction caractéristique du circuit reste constante. En conséquence, la fonction de sortie peut suit, en supposant que les registres R1 être déterminée comme et R1' ont des états initiaux rlo et rl'o respectivement de 0 et 1 : Ft0 = rlo.co xorrro.co = co xor Co = 0 Ft1 = (ao.bo.c1)xor( (ao + ID()) .c1) = 0 être initialement au pourrait Bien entendu, dans des variantes de réalisation, rlo niveau logique 0. La figure 7 représente schématiquement un exemple d'un dispositif pour mettre en oeuvre les procédés décrits en relation avec les figures 3 à 5. En particulier, le dispositif 700 comprend par exemple un dispositif de traitement 702 comprenant un ou plusieurs processeurs. Le dispositif de traitement 702 est commandé par une mémoire d'instructions 704, les instructions amenant le dispositif de traitement 702 à mettre en oeuvre un ou plusieurs des procédés décrits ici. Le dispositif de traitement 702 est également par exemple couplé à un dispositif de mémorisation 706 mémorisant les représentations de circuit. Un affichage 708 est également par exemple couplé au dispositif de traitement 702, permettant à des représentations de circuit d'être affichées, et/ou de tester niveau logique 1, et r110 au B11702 18 les résultats de l'équivalence fonctionnelle. Un ou plusieurs dispositifs de sortie 710 peuvent être également être prévus tel qu'un clavier, une souris, une interface réseau, etc. Un avantage des modes de réalisation décrits ici est que, en déterminant le nombre d'itérations permettant à chaque état atteignable d'être introduit dans une représentation de circuit sur la base d'un nombre réduit de registres et/ou d'un nombre réduit de variables d'entrée, le traitement peut être notablement simplifié et rendu très efficace temporellement. En outre, il est particulièrement avantageux de baser le calcul sur des groupes consistant en un nombre premier de registres supérieur à 1, tel que 3, 5 ou 7. Diverses variantes, modifications et améliorations aux modes de réalisation décrits ci-dessus apparaîtront facilement à l'homme de l'art. Par exemple, il sera clair pour l'homme de l'art que, bien que plusieurs exemples des paramètres r et mvar aient été fournis, il y a de nombreuses combinaisons distinctes de ces paramètres qui pourraient être utilisées, en fonction de la taille et de la nature des représentations de circuit à tester. En outre, il n'est pas nécessaire que la même valeur de r et/ou de mvar soit utilisée quand on traite des parties différentes des représentations de circuit. On outre, il sera clair pour l'homme de l'art que, pour simplifier encore les calculs, les processus des figures 3 et 5 pourraient s'appliquer à une partie d'une représentation de circuit. Les procédés des figures 3 et 5 pourraient par exemple ensuite être appliqués à d'autres parties de la représentation de circuit. Par exemple, une étape de concordance de registres est initialement mise en oeuvre pour définir des régions des représentations de circuit. Chaque ensemble de registres accordés forme alors une partie qui est traitée séparément selon le procédé des figures 3 et 5. En outre, bien que, dans l'exemple de réalisation de 35 la figure 5, le nombre N de registres soit divisé par le B11702 19 paramètre r pour déterminer le nombre x de groupes de registres, dans des variantes de réalisation, le nombre de registres dans chaque jème groupe peut ne pas être égal et peut être déterminé de façon différente. Par exemple, le premier groupe pourrait 5 comprendre 3 registres, le second groupe 5 registres, le troisième groupe 7 registres, etc. Le nombre de registres de chaque groupe pourrait également être choisi de façon aléatoire. D'autres critères utilisés pour sélectionner les registres formant chaque jème groupe pourraient également être pris en 10 compte tel que la dépendance structurelle entre les registres. En outre, bien que, en relation avec la figure 5, on ait décrit qu'un second appel du procédé est réalisé avec de nouvelles valeurs des paramètres r et/ou mvar, il sera clair pour l'homme de l'art qu'une telle vérification est optionnelle 15 et, dans certains modes de réalisation, aucun second appel ne pourrait être mis en oeuvre. En outre, dans d'autres modes de réalisation, des vérifications supplémentaires pourraient être réalisées, par exemple une troisième ou encore d'autres appels du procédé avec d'autres nouvelles valeurs de r et/ou de mvar. REVENDICATIONS1. Procédé de conception de circuit comprenant la vérification par un dispositif de traitement de ce que des première et seconde représentations de circuit (201, 202) sont fonctionnellement équivalentes comprenant : déterminer un nombre minimum de transitions d'états de la première représentation de circuit pour atteindre tous ses états en : a) calculant par le dispositif de traitement pour chaque première et seconde itérations successives d'au moins une partie de la première représentation de circuit, une première fonction caractéristique associée à un premier groupe de r registres et sur la base d'un nombre mvar de variables d'entrée, où r et mvar sont des entiers supérieur ou égal à 1, r étant inférieur au nombre total de registres dans la première représentation de circuit, et/ou mvar étant inférieur au nombre total d'entrées de la première représentation de circuit ; b) comparant les premières fonctions caractéristiques - calculées pour le premier groupe de registres pour les première et seconde itérations successives; et c) si les premières fonctions caractéristiques concordent, déterminant le nombre minimal de transitions d'états sur la base du nombre d'itérations réalisées jusqu'à la seconde itération ; et comparer les sorties des première et seconde représen- tations de circuit pour le nombre minimal de transitions d'états. 2. Procédé selon la revendication 1, dans lequel la première fonction caractéristique est calculée pour le premier 30 groupe de r registres et une seconde fonction caractéristique est calculée pour au moins un second groupe de r registres. 3. Procédé selon la revendication 2, dans lequel la détermination d'un nombre minimal de transitions d'états de la première représentation de circuit comprend en outre un seCondB11702 21 la seconde fonction de r' registres, r' appel des étapes a) à c) sur la base de caractéristique associée à un autre groupe étant un entier avec ri>r. des revendications 1 des revendications 1 4. Procédé selon l'une quelconque à 3, dans lequel r est un nombre premier. 5. Procédé selon l'une quelconque à 4, dans lequel l'étape a) est réalisée pour x groupes de registres, x étant égal à la partie entière par excès de (N/r), N étant le nombre total de registres. 10 6. Procédé selon l'une quelconque des revendications 1 à 5, dans lequel la première fonction caractéristique est produite sur la base d'une substitution d'au moins une valeur d'entrée de la représentation de circuit par une valeur fixée. 7. Procédé selon la revendication 6, dans lequel la 15 valeur d'entrée est fixée à une valeur déterminée et/ou à la valeur d'une autre valeur d'entrée du circuit. 8. Procédé selon l'une quelconque des revendications 1 à 7, dans lequel chaque itération de la partie de la première représentation de circuit comprend une duplication des entrées 20 et le placement des fonctions d'entrée de chacun des registres à leurs sorties. 9. Dispositif de traitement agencé pour mettre en oeuvre le procédé de la revendication 1. 10. Dispositif de mémorisation lisible par ordinateur 25 mémorisant un programme d'ordinateur comprenant des instructions qui, quand elles sont exécutées par un ordinateur, amènent le procédé selon l'une quelconque des revendications 1 à 8 à être mis en oeuvre.