21 / 24 · Concepto
Combina un marcador de referencia con invariantes locales
Comprueba valores, orden, ocupación y estabilidad durante las detenciones a partir de las transacciones aceptadas.
Las lecciones se pueden leer gratis. Inscríbete para guardar el progreso.
Basa la verificación en la aceptación de entradas
Un marcador de referencia calcula un resultado esperado para cada entrada aceptada y lo encola. En la entrega de salida, compara el elemento esperado más antiguo. Calcular directamente a partir del contrato, en vez de reproducir cada registro segmentado, reduce errores compartidos. Añade entradas solo al producirse una negociación de entrada; una entrada presentada pero rechazada no es trabajo pendiente.
Para las entradas ADD aceptadas tag10:(250,10) y tag11:(3,5), espera [(10,4,carry1),(11,8,carry0)]. Una salida válida pero detenida no retira ninguna entrada. Entregar tag10 retira solo esa entrada. Un tag10 repetido o el valor 8 etiquetado como 12 es incorrecto aunque algunos números coincidan. Incluye todos los indicadores y campos acompañantes pertinentes.
| Comprobación | Ejemplos de fallos |
|---|---|
| Salida frente a la cola de referencia | Aritmética, orden, etiquetas equivocadas |
| Accepted-delivered=occupancy | Pérdida, duplicación, entrega falsa |
| Carga útil detenida estable | Sobrescritura antes de la aceptación |
| Ocupación dentro de los límites | Desbordamiento o extracción de FIFO vacía |
| Cola de referencia vacía después del drenaje | Resultado final ausente |
Los invariantes locales identifican el primer flanco que falla, en lugar de solo una discrepancia final. La ocupación interna es el contador de FIFO más los bits de validez de etapas. Añade contabilidad de cancelación cuando se admita reinicio o vaciado y usa la misma política de flancos en ambos monitores.
Combina límites numéricos con casos temporales: cero, valores máximos, acarreo y préstamo, tráfico consecutivo, burbujas, detenciones largas, reemplazo con ocupación completa y drenaje final. Registra semillas aleatorias para repetir los fallos. Recorre exhaustivamente espacios de control pequeños cuando sea práctico.
Las comprobaciones de finalización necesitan un supuesto de progreso y un tiempo límite. Cuando el receptor pasa a estar permanentemente listo, el trabajo pendiente debe drenarse. Bajo detenciones indefinidas, exige conservación y ocupación acotada. Corromper deliberadamente el acarreo o el retardo de etiqueta debe hacer fallar las comprobaciones; esta prueba de mutación mide la sensibilidad. Superar modelos Node no valida el cableado HDL, el comportamiento X/Z, los cruces entre dominios de reloj ni la temporización de la implementación. Informa solo del alcance de ejecución observado realmente.
Inténtalo tú
Accepted=9 y delivered=5. El contador de FIFO es dos y ambas etapas son válidas. ¿Es coherente la contabilidad? Si se acepta otra entrada sin entrega y la ocupación sigue en cuatro, ¿qué ocurrió probablemente?
Leer la explicación
La contabilidad coincide: 9-5=2+1+1=4. Tras otra aceptación sin entrega, la diferencia pasa a cinco. Una ocupación de cuatro sugiere admisión sin capacidad o un elemento sobrescrito. Examina la disponibilidad en el primer flanco que falle.