12 / 37 · Concept

Vérification du MUX : tests exhaustifs et propriétés

Vérifier séparément couverture combinatoire et stockage, puis minimiser les contre-exemples.

Que signifie « correct » ?

Les entrées d'un bit a, b et sel donnent huit combinaisons : les tester toutes est efficace. Pour une largeur W, l'espace complet d'un MUX^{Multiplexeur Circuit combinatoire reliant une entrée parmi plusieurs à la sortie selon une sélection. La correspondance entre bits de sélection et numéro d'entrée doit être spécifiée. En savoir plus} contient $2^{2W+1}$ cas, sélection comprise ; une autre stratégie devient vite nécessaire.

Pour chaque bit d'une sortie de largeur W :

\forall i\in\{0,\ldots,W-1\},\quad y_i=\overline s a_i+s b_i

Choisir les stimuli selon le défaut recherché

Défaut	Entrée ou observation utile
a et b inversés	Données différentes, comparer sel=0 et sel=1
Ordre des bits inversé	Motifs à un seul bit à 1, walking-one
Bit bloqué	Tous à 0, tous à 1, bits alternés
Mauvais front de stockage	Modifier entre les fronts et vérifier le maintien de q
Décalage d'un cycle	Attendus différents sur des fronts consécutifs

Le nombre de tests ne suffit pas : expliquez quels défauts ils doivent détecter.

La comparaison ci-dessous retient uniquement a≠b. Chaque colonne est un vecteur. La sélection incorrecte produit l'opposé de expected dans les quatre cas.

Quatre combinaisons pour détecter l'inversion de sélection

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
a	`0.1.`
b	`1.0.`
sel	`0101`
expected	`01.0`
défaut inversé	`10.1`

Une référence indépendante de la réalisation

Copier le code du DUT peut reproduire son erreur. Construisez l'attendu depuis la table de vérité^{Table de vérité Tableau énumérant toutes les combinaisons d'entrée et leur sortie. Les évolutions temporelles s'examinent séparément sur un chronogramme. En savoir plus} ou une sélection par indice et suivez séparément l'état précédemment capturé de q. En cas de mismatch, réduisez la séquence au plus court contre-exemple qui conserve l'échec et expliquez sa cause.

Au lieu de comparer seulement l'état final, notez entrée, obtenu et attendu à chaque observation. Ces preuves distinguent « la simulation a tourné » de « la spécification est satisfaite ».

Essayez vous-même

Un MUX huit bits est testé pour les deux sélections uniquement avec a=0x00 et b=0xFF. Cela détecte-t-il une inversion de l'ordre des bits de sortie ?

Lire l’explication

Non. Inverser l'ordre des bits ne change ni 0x00 ni 0xFF. Utilisez des motifs positionnels comme 0x01 et 0x02, puis comparez chaque bit de sortie.