25 / 37 · Concept
Plan de vérification, couverture et référence indépendante
Distinguer tests réussis et contrat satisfait, puis intégrer limites, croisements et contre-exemples minimaux.
Les leçons sont gratuites. Inscrivez-vous pour enregistrer vos progrès.
Transformer la spécification en assertions vérifiables
Remplacez « fonctionne bien » par état après reset, sortie normale, maintien à l'arrêt, traitement d'une entrée interdite ou instant d'achèvement. Associer au moins un test et une observation à chaque affirmation révèle les omissions.
| Affirmation | Stimulus | Observation |
|---|---|---|
| Reset prioritaire | reset=enable=1 | État suivant initialisé |
| Ordre préservé | Motifs asymétriques continus | Valeurs et valid de toutes les sorties |
| Rebouclage exact | Autour du maximum | M−1→0, aucune valeur hors plage |
| Maintien à l'arrêt | Entrées variables, accept=0 | État inchangé |
| Recouvrement des motifs | 10101 | Détection aux entrées acceptées 3 et 5 |
Pourquoi une référence indépendante ?
Copier les mêmes tranchesTranche Sélection d'une plage contiguë de bits d'un vecteur. La plage choisie fixe largeur et ordre des bits du résultat. En savoir plus d'un RTL à décalage peut copier l'erreur d'indice. Une autre formulation, par multiplication/modulo ou comparaison de suffixe de chaîne, aide à croiser les vérifications. Une forme différente ne prouve toutefois pas l'indépendance : contrôlez de petits cas à la main.
La couverture n'est pas le nombre de tests réussis
Exécuter toutes les lignes de code ne signifie pas tester tous les cas fonctionnels. Les croisements reset×enable, state×input ou full×push×pop peuvent révéler des erreurs. Complétez l'aléatoire par des tests dirigés des cas rares et essentiels.
Un circuit combinatoire à N entrées offre cas, mais un circuit séquentiel possède aussi des séquences temporelles. Analysez atteignabilité et conservation des invariantsInvariant Condition devant rester vraie dans toute exécution autorisée. Par exemple, l'occupation d'un FIFO de profondeur 4 reste toujours entre 0 et 4. à chaque transition. Une simulation finie réussie n'est pas une preuve mathématique sur un temps illimité.
Calculez l'attendu indépendamment depuis le contrat. Lors d'un échec, gardez aussi l'entrée et l'état précédents, pas seulement la sortie réelle.
- Spécification et stimuli: Choisir les limites et combinaisons de conditions
- Modèle de référence indépendant: Calculer la valeur attendue et son instant de validité
- Comparer au DUT: Comparer au même instant d'observation
- Consigner le premier écart: Conserver le contre-exemple minimal et la graine
Réduire et consigner l'échec
Enregistrez état précédent, entrée, attendu et obtenu du premier mismatch. Retirez les stimuli inutiles pour obtenir un contre-exemple minimal, puis corrigez. Rejouez aussi les anciennes vérifications de limites et de resetReset Commande ramenant l'état à la valeur initiale spécifiée. Son caractère synchrone/asynchrone et sa priorité sur les autres commandes doivent être définis. En savoir plus, pas seulement le test modifié.
Essayez vous-même
La couverture RTL est de 100 % et 10 000 tests aléatoires passent, mais reset et enable n'ont jamais été à 1 ensemble. Que faut-il ajouter ?
Lire l’explication
Vérifiez ce croisement dans le contrat et ajoutez un test dirigé depuis un état non nul révélant la priorité. Couverture de code et nombre de tests ne remplacent pas la vérification d'une condition fonctionnelle précise.