27 / 63 · Concetto

Verifica del MUX: esaustività e proprietà

Verificare separatamente copertura combinatoria e memoria e minimizzare i controesempi.

Che cosa considerare corretto?

Con dati a un bit a, b e selezione sel esistono otto combinazioni: una verifica esaustiva è efficiente. Per un MUX^{Multiplexer Circuito combinatorio che collega un ingresso all’uscita secondo la selezione. Va specificata la corrispondenza fra bit di selezione e ingressi. Approfondisci} largo W, includendo la selezione servono $2^{2W+1}$ casi; aumentando anche poco la larghezza occorrono altre strategie.

La regola per ogni bit d'uscita è:

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

Scegliere gli stimoli secondo il difetto

Difetto da cercare	Ingresso o osservazione utile
a/b scambiati	a, b diversi, confronto con sel=0 e 1
Ordine dei bit invertito	Walking-one con un solo bit a 1
Stuck-at	Tutti 0, tutti 1, bit alternati
Fronte di memoria errato	Cambiare ingressi fra i fronti e controllare q fermo
Ritardo errato di un ciclo	Attesi diversi a fronti consecutivi

Molti test non bastano a rendere buona una verifica. Dovete spiegare quale difetto intendete rilevare.

Il confronto seguente usa solo a≠b. Ogni colonna è un vettore; la selezione errata produce l'opposto di expected in tutte e quattro.

Quattro combinazioni per rilevare la selezione invertita

Mostra i dati della forma d’onda

Dati della forma d’onda: ogni carattere è un intervallo; il punto mantiene lo stato precedente; p è un ciclo di clock.
Segnale	Forma d’onda	Valori del bus
a	`0.1.`
b	`1.0.`
sel	`0101`
expected	`01.0`
swapped bug	`10.1`

Costruire un riferimento indipendente

Copiare il codice del DUT può duplicare l'errore. Ricavate i valori attesi dalla tabella di verità^{Tabella di verità Elenco completo delle combinazioni d’ingresso e delle rispettive uscite. Le variazioni temporali si esaminano separatamente nelle forme d’onda. Approfondisci} o da una selezione per indice e seguite separatamente lo stato campionato q. In caso di mismatch riducete la sequenza al più breve esempio che conserva il guasto e spiegatene la causa.

Registrate a ogni osservazione valore reale, atteso e ingressi, invece del solo finale. Questo distingue «la simulazione è stata eseguita» da «la specifica è soddisfatta».

Prova tu

Un MUX a otto bit è provato solo con a=0x00, b=0xFF per entrambe le selezioni. Rileva l’ordine dei bit d’uscita invertito?

Leggi la spiegazione

No. 0x00 e 0xFF restano uguali invertendo i bit. Usate schemi che mostrano la posizione, come 0x01 e 0x02, e confrontate ogni bit d’uscita.