Vérification des circuits numériques. Revue

Je vais essayer de parler en général de la vérification des circuits numériques.

La vérification dans ce domaine est un processus important qui nécessite la participation d'ingénieurs expérimentés. Par exemple, un spécialiste de la vérification travaillant sur des systèmes avec un processeur doit, en règle générale, posséder des langages de script et des langages de shell de commande (Tcl, bash, Makefile, etc.), des langages de programmation (C, C ++, assembleur), HDL / HDVL (SystemVerilog [10, Annexe C - Histoire du langage] [11], Verilog, VHDL), méthodologies et cadres modernes (UVM).

La proportion de temps consacré à la vérification atteint 70 à 80% du temps total du projet. L'une des principales raisons de cette attention est que vous ne pouvez pas publier un "patch" sur la puce après sa mise en production, vous ne pouvez publier que des "errata de silicium" (cela ne s'applique pas aux projets FPGA / FPGA).

Par circuits numériques, je veux dire:

• blocs fonctionnels complexes / propriétés intellectuelles (SFB / IP);
• Puces personnalisées de circuits intégrés spécifiques à l'application (ASIC)
• circuits intégrés logiques programmables / réseau de portes programmables sur site (FPGA);
• systèmes sur puce / système sur cristal (SoC / SoC);
• etc.

Problèmes de vérification réels

L'état actuel et les tendances dans le domaine de la vérification peuvent être jugés par les défis et problèmes suivants auxquels il est confronté [6]:

• La taille de l'objet de vérification (OB) est en constante augmentation. Même un petit CI de type microcontrôleur est un ensemble de dizaines de sous-modules, très souvent avec des fonctionnalités complexes. Les grands circuits intégrés sont des complexes dans lesquels il peut y avoir jusqu'à des dizaines de milliards de transistors, et le schéma de gestion de l'alimentation à lui seul peut dépasser la complexité de certains processeurs [8];
• il est impossible d'établir un cahier des charges pour IMS au début du projet et de ne le suivre qu'à l'avenir, il évolue constamment tout au long du processus de développement (le client modifie les exigences, les problèmes techniques ou la découverte de solutions plus optimales nous obligent à reconsidérer les approches, etc.). Sur cette base, tous les processus devraient percevoir la dynamique des changements de spécification et être modifiés conformément aux exigences;
• souvent, plusieurs équipes éloignées les unes des autres travaillent sur la vérification des projets, dont le nombre peut atteindre des dizaines de personnes;
• le nombre de tests individuels et leurs types atteint un nombre énorme, leurs résultats doivent être collectés et analysés;
• la modélisation même de systèmes numériques nécessite beaucoup de temps informatique;
• l'exhaustivité des objectifs de préparation établis pour le projet dépend en grande partie de la compétence et de l'intuition des spécialistes de la vérification;
• malgré l'existence d'indicateurs de couverture du projet avec des tests (métriques), la seule façon de compléter la vérification est de décider de la suspendre, basée principalement sur les conclusions suivantes: l'argent ou le temps consacré à l'étape du projet doit être mis en production, il semble qu'ils aient atteint une couverture de code de 100 %, nous testons depuis une semaine et nous n'avons trouvé aucune erreur, etc.

Types de vérification

La vérification des circuits numériques peut être divisée selon les principaux types suivants:

1. fonctionnel (vérification fonctionnelle) - le nom parle de lui-même, vous vérifiez si votre système exécute correctement ses fonctions;
2. vérification formelle - avec cette vérification, l'équivalence des représentations de votre système à différentes étapes du parcours de conception ou la réalisation des déclarations placées dans le code source est établie:
   
   • Vérification d'équivalence (par exemple RTL-to-RTL, RTL-to-Gate, Gate-to-Gate);
   • Vérification des propriétés (vérification du modèle) (vérifie les propriétés (assertions) spécifiées dans le code à l'aide de SVA (par exemple)).
3. analyse de code statique - vérification du code source selon des critères formels de conformité aux règles d'utilisation du langage et de ses constructions. Très souvent, les règles de vérification configurées sont envoyées à RMM [4]. Les programmes pour une telle vérification sont généralement appelés charpie ou linter;
4. vérification physique - implique essentiellement des contrôles DRC, LVS, PERC, etc., la performance physique du système est vérifiée pour la conformité aux normes technologiques et la conformité aux représentations physiques et logiques, etc. La composition des chèques dépend fortement de la technologie. En règle générale, la vérification physique est effectuée par un ingénieur ou une équipe de conception topologique.
5. prototypage - l'utilisation de FPGA pour la vérification fonctionnelle [18].

La vérification fonctionnelle dans le cadre de tous les travaux est la plus importante et nécessite une implication humaine directe.

L'analyse de code statique ne nécessite qu'une configuration initiale des outils, ce qui correspond aux règles de conception interne adoptées par l'entreprise, puis l'outil est engagé dans le fait qu'il fournit des «précieux conseils» aux développeurs et ne nécessite pas de supervision constante.

Les outils de vérification formels sont souvent également très indépendants, ils ne nécessitent qu'une analyse minutieuse des rapports qu'ils génèrent. Ils conviennent également à l'ingénierie inverse, lorsque, pour une raison quelconque, vous savez que vous devez restaurer le code à partir de la liste des circuits.

Exemples d'outils de vérification

Exemples d'outils de vérification de circuits numériques (route numérique sur le dessus):

• outils de gestion de la vérification
  
  • Mentor Graphics - Questa Verification Management
  • Cadence - vManager
  • Synopsys - Verdi, VC Execution Manager («ExecMan»)
• fonctionnel - généralement des simulateurs
  
  • Graphiques du mentor - ModelSim, QuestaSim
  • Cadence - Incisive, Xcelium
  • Synopsys - VCS
  • Logiciels gratuits de développeurs indépendants - simulateurs Verilator, Icarus [5]
• formel
  
  • Mentor Graphics - Formal Pro, Questa Formal Verification
  • Cadence - JasperGold, Conformal LEC, Incisive Formal Verification Platform
  • Synopsys - Formalité, VC formel
• analyse de code statique
  
  • Graphiques du mentor - Questa AutoCheck
  • Cadence - HAL, JasperGold
  • Synopsys - SpyGlass Lint
• vérification physique
  
  • Graphisme du mentor - Calibre
  • Cadence - Pegasus, Système de vérification physique,
  • Synopsys - Hercules, IC Validator

Méthodes de vérification fonctionnelle

Vérification fonctionnelle - est un ensemble de tests, je vais conditionnellement me permettre d'être divisé en trois groupes (ce n'est pas un dogme, c'est une expérience personnelle):

1. Branches positives - vérification du comportement dans des situations normales, réglementée par la spécification de l'appareil ou de la norme, etc. C'est-à-dire Nous vérifions les situations où tout se passe bien.
2. Branches négatives - vérification des écarts par rapport aux situations standard, mais dans le cadre d'une spécification ou d'une norme, par exemple - un décalage de la somme de contrôle, du nombre de données reçues, etc. C'est-à-dire quand quelque chose ne va pas, mais nous savions que cela pouvait être et nous savons comment travailler dans cette situation.
3. Situations non standard - toutes les situations aléatoires allant des violations des protocoles de communication, de l'ordre des données aux collisions physiques dans les interfaces, des changements aléatoires de l'état des éléments logiques, etc. C'est-à-dire C'est à ce moment que tout peut arriver et vous devez vous assurer que l'OB sortira après cela en état de fonctionnement.

Les deux premières étapes peuvent être automatisées en utilisant UVC / VIP (Universal Verification Component / Verification IP) et assez rapidement, vous pouvez augmenter le volume de divers tests, y compris ceux générés automatiquement. La troisième étape est un «chef-d'œuvre» en vérification, cette étape nécessite une approche et une expérience extraordinaires, elle est très difficile à automatiser, car la plupart des situations sont un algorithme distinct, peut-être un script de CAO ou des instructions pour les vérifications "manuelles".

Types de métriques de vérification fonctionnelle

Les mesures sont des indicateurs de la couverture de test d'un projet. Ils sont nécessaires pour comprendre quels autres tests doivent être développés pour vérifier les situations possibles et combien de temps la vérification peut prendre [16].

Malheureusement, un seul type de métrique est évalué sur la base du code source du projet, la définition des critères pour les types restants est le résultat d'un travail intellectuel.

De plus, il faut se rappeler que l'atteinte des indicateurs souhaités par un type de métrique ne signifie pas maniabilité en général, il faut toujours évaluer le complexe.

Types de métriques [3]:

• revêtement fonctionnel . Montre combien la fonction OB a été testée. Les critères de cette couverture peuvent être déterminés par le plan de test et l'introduction de constructions spéciales (groupe de couverture [1]) dans l'environnement de test et / ou OM, qui contrôlent si telle ou telle fonction / action a été exécutée ou non, si les données ont changé d'une certaine manière, etc. Les informations des conceptions intégrées dans le code source peuvent être automatiquement collectées par CAD.
• couverture du code - modification de l'état des constructions du code source pendant les tests. Il est collecté automatiquement par CAD, ne nécessite l'introduction d'aucune structure dans le code source. Par exemple:
  
  • registres de commutation (Toggle Coverage);
  • l'activité de chaque ligne de code (couverture de ligne);
  • l'activité des expressions (Statement Coverage), en fait - il s'agit de Line Coverage, mais peut suivre les expressions qui sont plus d'une ligne dans l'éditeur;
  • activité d'un segment de code à l'intérieur d'une instruction ou procédure conditionnelle (Block Coverage), une variation de Statement Coverage;
  • activité de toutes les branches d'instructions conditionnelles telles que if, case, while, repeat, forever, for, loop (Branch Coverage);
  • changement de tous les états (vrai, faux) des expressions logiques des composants (couverture d'expression);
  • état de la machine d'état (couverture des machines à états finis).
• couverture des sinistres . Les instructions sont des constructions de langage spéciales qui suivent divers événements et séquences et, selon des critères spécifiés, déterminent la légalité de leur occurrence.

Méthodes de vérification fonctionnelle

Méthode des tests dirigés (DTM)

Des tests directs et significatifs. Si cette méthode est adoptée dans le projet, alors le plan de vérification est composé de tests visant à vérifier le comportement de l'OM à des points d'intérêt spécifiques (états). La vérification de toutes les situations possibles, en particulier dans les projets complexes, est presque impossible.
Dans le même temps, les problèmes pouvant survenir dans des situations non couvertes par les tests ne sont pas détectés avant le démarrage de l'appareil pour une utilisation dans des conditions réelles. En règle générale, ces tests utilisent des mesures de couverture fonctionnelle.

Vérification basée sur la couverture, vérification basée sur les mesures (CDV, MDV) [17]

Le concept de création de tests visant à atteindre une certaine «couverture de test» des substances organiques. Ils s'appuient sur des métriques pour comprendre quels tests doivent être ajoutés au plan de vérification afin d'atteindre les objectifs de préparation du projet.
Vous devez utiliser des outils d'analyse de couverture pour voir quoi ajouter au plan de vérification. En fait, si vous commencez à ajuster le plan de vérification dans le DTM, en vous appuyant au moins sur la «couverture du code», alors nous pouvons déjà supposer que le DTM est passé en douceur au CDV.

Vérification aléatoire contrainte (CRV)

Vérification en soumettant des influences aléatoires. Ce sont vraiment des tests automatiques avec la génération d'effets aléatoires sur l'OM, ​​mais il est difficile de les imaginer sans symbiose avec ABV.
La méthode est très coûteuse au début, car Il faut beaucoup de temps pour préparer les outils. Une fois la phase initiale de préparation terminée, le test peut être démarré automatiquement, à plusieurs reprises avec différentes données initiales. Si une incompatibilité d'assertion est détectée, l'équipe de développement et de vérification commence à analyser l'erreur détectée.
Dans un vrai projet, on ne peut pas se limiter uniquement à cette méthode, car En utilisant cette méthode, vous pouvez collecter la couverture du code et la couverture des instructions, et ils ne peuvent rien dire sur le bon fonctionnement du système d'exploitation, c'est-à-dire respect des spécifications. Il doit être complété par des tests fonctionnels.
La mise en œuvre de cette méthodologie nécessite:

1. implémenter «l'assertion» dans tous les points importants du code source de l'OB et de l'environnement de test;
2. développer des générateurs d'effets aléatoires et des scénarios de leur travail, c'est-à-dire les impacts sont aléatoires, mais ont des limites de portée (nous n'avons pas le temps de tout trier), l'ordre de classement, etc.

Vérification basée sur les assertions [9] (ABV)

Vérification avec relevés. Probablement, ce n'est même pas une méthode indépendante, mais un composant ou un composant de base de ce qui précède.

Un problème important avec ABV est de savoir comment distribuer les assertions, lesquelles sont les mieux placées dans le code source de l'OB, lesquelles devraient être dans l'environnement de test.

Il convient de noter tout de suite que le langage Verilog n'a pas d'assertions dans son standard (elles peuvent être créées en utilisant les constructions de langage de base, mais des directives sont nécessaires pour le synthétiseur afin qu'il ne gère pas leur conversion). Les assertions n'apparaissent que dans la norme SystemVerilog, et elles étaient également à l'origine dans la norme de langage VHDL et e.

Je vous suggère de vous familiariser avec les recommandations de spécialistes, y compris Clifford Cummings [12, articles sur SVA] sur la distribution des travaux sur leur écriture, ainsi que les documents sur ABV sur le site Web de la Verification Academy [13].

Les références

1. IEEE Std 1800TM-2012. Norme IEEE pour SystemVerilog - Unified Hardware Design, Specification, and Verification Language
2. Clive Maxfield. Conception FPGA. Architecture, outils et méthodes. Le parcours du jeune combattant. ISBN 978-5-94120-147-1 (RUS), ISBN 0-7506-7604-3 (ENG)
3. Académie de vérification. Livre de recettes de couverture. Couverture de test Pro
4. Michael Keating, Pierre Bricaud. Réutiliser le manuel de méthodologie pour les conceptions de systèmes sur puce. Imprimé ISBN 1-4020-7141-8, eBook ISBN 0-306-47640-1
5. Liste des CAO sous licence et librement distribués
6. Graphiques du mentor. Un exemple de statistiques sur l'état actuel et l'étendue de la vérification
7. WikiChip. Chips Wikipedia
8. Wikipédia Données généralisées sur le nombre de transistors dans le CI
9. Harry Foster, Adam Krolnik, David Lacey. Conception basée sur les assertions Imprimé ISBN 1-4020-8027-1, eBook ISBN 1-4020-8028-X
10. Stuart Sutherland, Simon Davidmann, Peter Flake. SystemVerilog for Design. Imprimé ISBN-10: 0-387-33399-1, eBook ISBN-10: 0-387-36495-1
11. Chris Spear, Greg Tumbush. SystemVerilog pour vérification. Imprimé ISBN: 978-1-4614-0714-0, eBook ISBN: 978-1-4614-0715-7
12. Conception Sunburst. Papiers
13. Académie de vérification. Cours ABV
14. Doulos. Documents utiles en ligne et ouvrages de référence
15. Prakash Rashinkar, Peter Paterson, Leena Singh. Vérification du système sur puce. méthodologie et techniques. Impression ISBN: 0-792-37279-4, eBook ISBN: 0-306-46995-2
16. Académie de vérification. Mesures dans la vérification SoC
17. Doulos. Méthodologie de vérification axée sur la couverture
18. Doug Amos, Austin Lesea, René Richter. Manuel de méthodologie de prototypage basé sur FPGA: Meilleures pratiques en conception pour le prototypage (FPMM). Print ISBN: 978-1617300042. Télécharger gratuitement depuis le site Web de Synopsys