Combine um scoreboard com invariantes locais

Baseie a verificação na aceitação de entradas

Um scoreboard calcula um resultado esperado a partir de cada entrada aceita e o enfileira. Na entrega da saída, compare o item esperado mais antigo. Calcular diretamente a partir do contrato em vez de reproduzir cada registrador do pipeline reduz erros compartilhados. Adicione entradas apenas em um handshake de entrada; uma entrada apresentada, mas rejeitada, não é trabalho pendente.

Para as entradas ADD aceitas tag10:(250,10) e tag11:(3,5), espere [(10,4,carry1),(11,8,carry0)]. Uma saída válida em pausa não remove uma entrada. Entregar tag10 remove apenas essa entrada. Uma tag10 repetida ou o valor 8 etiquetado como 12 está incorreto mesmo se alguns números coincidirem. Inclua todos os indicadores e campos acompanhantes relevantes.

Invariantes locais identificam a primeira borda com falha em vez de apenas uma diferença final. A ocupação interna é a contagem da FIFO mais os bits de validade dos estágios. Acrescente contabilização de cancelamentos quando reset ou flush forem permitidos e use a mesma política de bordas nos dois monitores.

Combine limites numéricos com casos de temporização: zero, valores máximos, carry e borrow, tráfego consecutivo, bolhas, pausas longas, substituição com fila cheia e esvaziamento final. Registre sementes aleatórias para falhas reproduzíveis. Esgote pequenos espaços de controle quando for viável.

Verificações de conclusão precisam de uma premissa de progresso e de um tempo limite. Quando o destino se tornar permanentemente pronto, o trabalho pendente deverá ser esvaziado. Sob pausas indefinidas, exija preservação e ocupação limitada. Corromper deliberadamente o carry ou o atraso da etiqueta deve fazer as verificações falharem; esse teste de mutação mede a sensibilidade. A aprovação de modelos em Node não valida conexões HDL, comportamento X/Z, cruzamento de domínios de clock nem temporização da implementação. Informe apenas o escopo de execução realmente observado.