12 / 37 · Concepto

Verificación del MUX: prueba exhaustiva y propiedades

Compruebe por separado la cobertura combinacional y el almacenamiento y reduzca los contraejemplos.

Qué significa que sea correcto

a, b y sel de un bit tienen ocho combinaciones: probarlas todas es eficiente. Para un MUX^{Multiplexor Circuito combinacional que conecta una de varias entradas a la salida según una señal de selección. Debe especificarse la correspondencia entre los bits de selección y los números de entrada. Más información} de ancho W, la enumeración ingenua necesita $2^{2W+1}$ combinaciones, por lo que anchos mayores requieren otra estrategia.

La selección de cada bit es:

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

Elija estímulos según el fallo buscado

Fallo	Entrada u observación útil
a y b intercambiadas	Datos distintos y ambas selecciones
Orden de bits invertido	Walking-one, un solo bit en 1
Bit atascado	Todo 0, todo 1 y bits alternos
Flanco de captura incorrecto	Cambiar entradas entre flancos y comprobar conservación de q
Error de un ciclo	Valores esperados distintos en flancos consecutivos

Muchas pruebas no bastan para una buena verificación: debe explicar qué fallo detecta cada una.

La comparación siguiente incluye solo a≠b. Cada columna es un vector; la selección incorrecta produce el opuesto de la referencia en las cuatro.

Cuatro combinaciones que detectan la selección invertida

Ver los datos de la forma de onda

Datos de la forma de onda: cada carácter es un intervalo; un punto conserva el estado anterior; p representa un ciclo de reloj.
Señal	Forma de onda	Valores del bus
a	`0.1.`
b	`1.0.`
sel	`0101`
esperado	`01.0`
selección invertida	`10.1`

Haga independiente el modelo de referencia

Copiar el código del DUT puede duplicar su error. Genere expectativas desde la tabla de verdad^{Tabla de verdad Tabla que enumera todas las combinaciones posibles de entradas y la salida de cada una. La evolución temporal se comprueba por separado en las formas de onda. Más información} o la selección por índice y siga por separado el estado capturado de q. Ante una discrepancia, reduzca la secuencia al caso más corto que aún falle y explique la causa.

Registre entrada, resultado y referencia en cada observación, no solo al final. Ese registro distingue «la simulación se ejecutó» de «se cumplió la especificación».

Inténtalo tú

Probó un MUX de 8 bits con a=0x00 y b=0xFF para ambas selecciones. ¿Esto también detecta inversión del orden de bits de salida?

Leer la explicación

No. 0x00 y 0xFF no cambian al invertir el orden de bits. Use patrones que revelen posiciones, como 0x01 y 0x02, y compare cada bit de salida.