26 / 37 · Concept
Déboguer un compteur avec un contre-exemple minimal
Construire des tests courts distinguant reset, enable et erreurs de rebouclage.
Les leçons sont gratuites. Inscrivez-vous pour enregistrer vos progrès.
Une valeur finale correcte peut cacher une mauvaise séquence
Finir à 0 ne prouve pas reset et rebouclage : un circuit bloqué à 0 donne aussi ce résultat. Observez séparément incrémentation, maintien, 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 et passage de la limite.
Faire volontairement coïncider deux fonctions
| Situation | Exigence à vérifier |
|---|---|
| reset=1, enable=0 | Le reset n'est pas masqué par enable |
| reset=1, enable=1 | Le reset prime sur l'incrémentation |
| count=M−1, enable=0 | Pas de rebouclage pendant l'arrêt |
| count=M−1, enable=1 | Retour exact de M−1 à 0 |
| Reset modifié entre les fronts | Application synchrone au prochain front |
Tester chaque commande seule révèle difficilement les erreurs de priorité.
Chaque colonne observe un front montantFront montant Instant où l'horloge passe de 0 à 1, distinct du niveau désignant tout l'intervalle CLK=1. En savoir plus, entrées avant et états after après mise à jour. Ce n'est pas un retard physiqueRetard de propagation Temps nécessaire après un changement d'entrée pour que la sortie se stabilise à sa valeur correcte. Équivalence logique et caractéristiques temporelles sont distinctes. En savoir plus. Avec count initial=5, le circuit erroné ne teste reset que sous enable et conserve donc 5 au premier front. Malgré une même valeur finale, le premier désaccord révèle le défaut.
Voir les données du chronogramme
| Signal | Forme d'onde | Valeurs du bus |
|---|---|---|
| edge | 234 | E0 → E1 → E2 |
| reset | 101 | |
| enable | 01. | |
| correct après | 234 | 0 → 1 → 0 |
| défaut après | 234 | 5 → 6 → 0 |
Commencez le modèle modulo-8 à 101. Choisissez enable=0, reset=1 et avancez l'horloge : la valeur correcte est 000, mais le RTL avec reset sous enable conserve 101. Relâchez reset, puis distinguez maintien à enable=0 et incrémentation à enable=1.
Le reset synchrone est prioritaire sur enable. Si enable=0, conserver la valeur mémorisée. q=101; q_next = (q + 1) mod 8
Trouver le premier désaccord avec une référence
Ce modèle fonctionnel suppose un état normal entre 0 et M−1. Ajoutez séparément la politique de récupération hors plage. Calculez l'attendu et comparez à chaque front. Les entrées et l'état juste avant le premier échec donnent le point de départ minimal du diagnostic.
Si l'échec apparaît après 1000 cycles, retirez les portions inutiles pour le reproduire en trois à cinq fronts. Gardez ce contre-exemple dans les tests de non-régression après correction. Relisez séparément spécification et code pour ne pas modifier conception et test selon la même condition erronée.
Essayez vous-même
Le code erroné place reset dans if(en) begin if(rst) ... end. Quels état initial et entrées donnent le contre-exemple le plus court ?
Lire l’explication
Partez d'un état non nul et appliquez un seul front montant avec rst=1,en=0. Le contrat reset prioritaire impose 0, mais le circuit erroné conserve l'ancien état. Partir de 0 masquerait le défaut.