12 / 37 · Conceito

Verificação do MUX: teste exaustivo e propriedades

Confira separadamente a cobertura combinacional e o armazenamento e reduza os contraexemplos.

O que significa estar correto

a, b e sel de um bit têm oito combinações: testar todas é eficiente. Para um MUX^{Multiplexador Circuito combinacional que conecta uma dentre várias entradas à saída conforme um sinal de seleção. É preciso especificar a correspondência entre os bits de seleção e os números das entradas. Saiba mais} de largura W, a enumeração direta exige $2^{2W+1}$ combinações, portanto larguras maiores precisam de outra estratégia.

A seleção de cada bit é:

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

Escolha estímulos conforme o defeito procurado

Defeito	Entrada ou observação útil
a e b trocadas	Dados diferentes e ambas as seleções
Ordem de bits invertida	Walking-one, apenas um bit em 1
Bit preso em um valor	Tudo 0, tudo 1 e bits alternados
Borda de captura incorreta	Mudar entradas entre bordas e conferir manutenção de q
Erro de um ciclo	Valores esperados diferentes em bordas consecutivas

Muitos testes não bastam para uma boa verificação: é preciso explicar qual defeito cada um detecta.

A comparação abaixo inclui apenas a≠b. Cada coluna é um vetor; a seleção incorreta produz o oposto da referência nas quatro.

Quatro combinações que detectam a seleção invertida

Ver os dados da forma de onda

Dados da forma de onda: cada caractere é um intervalo; um ponto mantém o estado anterior; p representa um ciclo de clock.
Sinal	Forma de onda	Valores do barramento
a	`0.1.`
b	`1.0.`
sel	`0101`
esperado	`01.0`
seleção invertida	`10.1`

Torne independente o modelo de referência

Copiar o código do DUT pode duplicar seu erro. Gere expectativas a partir da tabela-verdade^{Tabela-verdade Tabela que enumera todas as combinações possíveis de entradas e a saída de cada uma. A evolução temporal é verificada separadamente nas formas de onda. Saiba mais} ou da seleção por índice e acompanhe separadamente o estado capturado de q. Diante de uma discrepância, reduza a sequência ao caso mais curto que ainda falhe e explique a causa.

Registre entrada, resultado e referência em cada observação, não apenas no final. Esse registro distingue «a simulação executou» de «a especificação foi cumprida».

Experimente

Você testou um MUX de 8 bits com a=0x00 e b=0xFF nas duas seleções. Isso também detecta inversão na ordem dos bits de saída?

Ler a explicação

Não. 0x00 e 0xFF não mudam ao inverter a ordem dos bits. Use padrões que revelem posições, como 0x01 e 0x02, e compare cada bit de saída.