18 / 37 · Vérification

Bilan : largeur, priorité et limites du rebouclage

Évaluer limites et commandes simultanées à partir du contrat de transition.

Le contrat d'un compteur modulo-10

Pour count non signé^{Non signé Interprétation d'un motif de bits comme entier non négatif. Sur n bits, la plage va de 0 à 2^n−1 et peut différer de l'interprétation signée du même motif. En savoir plus} sur quatre bits, la priorité est reset, puis enable, puis maintien. reset impose 0 ; sinon, enable actif ramène les valeurs ≥9 à 0 et incrémente les autres.

N=\lceil\log_2 10\rceil=4

Quatre bits offrent seize états stockables, pas automatiquement une fonction à dix états. En particulier, count=9 avec enable=0 ne doit pas revenir à 0.

Chaque colonne observe un front montant^{Front montant Instant où l'horloge passe de 0 à 1, distinct du niveau désignant tout l'intervalle CLK=1. En savoir plus}, avec entrées avant et états after après. L'alignement représente les échantillons, pas le retard physique^{Retard 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=9, sans reset, la première colonne enable=0 conserve 9 ; seule la suivante avec enable=1 revient à 0.

Le maintien doit aussi être respecté aux valeurs limites

Voir les données du chronogramme

Données du chronogramme : chaque caractère représente un intervalle ; un point maintient l'état précédent ; p représente un cycle d'horloge.
Signal	Forme d'onde	Valeurs du bus
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count après	`23.4`	9 → 0 → 1

Exercices supplémentaires

Donnez l'état suivant pour count=9, reset=0, enable=0.
Expliquez la récupération depuis count=15 avec enable=1.
Définissez si une impulsion terminale doit apparaître pour count=9, reset=1, enable=1, sachant que les sorties sont définies à 0 pendant le reset^{Reset 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}.

Essayez vous-même

Combien de transitions à un pas couvrent tous les count=0–15 et les combinaisons reset/enable ? Ce test prouve-t-il automatiquement toutes les exigences sur de longues séquences ?

Lire l’explication

$16\times2\times2=64$ cas. Si count représente tout l'état et que transitions et sorties sont spécifiées exactement, cette vérification à un pas est une preuve forte. Elle ne prouve pas les exigences omises : initialisation, hypothèses d'entrée, état distinct d'une impulsion terminale ou timing réel.

Avec count=9, reset=1 et enable=1 sont échantillonnés ensemble. Quels count suivant et impulsion terminale respectent la priorité du reset ?

Choisissez une réponsecount=0, impulsion=1 : rebouclage normal.count=10, impulsion=0 : enable est prioritaire.count=0, impulsion=0 : reset initialise l'état et l'impulsion.