21 / 24 · Concept

Combiner un tableau de suivi avec des invariants locaux

Vérifiez valeurs, ordre, occupation et stabilité sous blocage à partir des transactions acceptées.

Ancrer la vérification sur l’acceptation d’entrée

Un tableau de suivi calcule un résultat attendu pour chaque entrée acceptée et le met en file. À la livraison d’une sortie, comparez l’élément attendu le plus ancien. Calculer directement à partir du contrat plutôt que reproduire chaque registre du pipeline réduit les erreurs communes. N’ajoutez des entrées que lors d’un transfert d’entrée synchronisé ; une entrée présentée mais refusée n’est pas du travail en cours.

Pour les entrées ADD acceptées tag10: (250, 10) et tag11: (3, 5), attendez [(10, 4, carry1), (11, 8, carry0)]. Une sortie valide mais bloquée ne retire pas d’entrée. Livrer tag10 retire seulement cette entrée. Un tag10 répété ou la valeur 8 étiquetée 12 est incorrect même si certains nombres correspondent. Incluez tous les drapeaux et champs associés pertinents.

Vérification	Exemples d’échecs
Sortie comparée à la file de référence	Arithmétique, ordre, mauvaises étiquettes
Accepted-delivered=occupancy	Perte, duplication, fausse livraison
Charge utile bloquée stable	Écrasement avant acceptation
Occupation dans les limites	Débordement ou sous-remplissage illégal de FIFO
File de référence vide après vidange	Dernier résultat manquant

Les invariants locaux identifient le premier front défaillant plutôt qu’un seul écart final. L’occupation interne est le compteur FIFO plus les bits de validité des étages. Ajoutez le bilan d’annulation lorsque reset ou flush est permis, avec la même politique de front dans les deux observateurs.

Combinez les limites numériques et les cas temporels : zéro, valeurs maximales, retenue et emprunt, trafic consécutif, bulles, longs blocages, remplacement à plein et vidange finale. Notez les graines aléatoires pour reproduire les échecs. Explorez exhaustivement les petits espaces de commande lorsque c’est pratique.

Les vérifications de fin nécessitent une hypothèse de progression et un délai maximal. Une fois le récepteur définitivement prêt, le travail en cours doit se vidanger. Sous blocages indéfinis, exigez plutôt conservation et occupation bornée. Corrompre délibérément la retenue ou le retard d’étiquette doit faire échouer les vérifications ; ce test par mutation mesure leur sensibilité. Réussir les modèles Node ne valide ni câblage HDL, ni comportement X/Z, ni franchissement de domaines d’horloge, ni temporisation d’implémentation. Ne rapportez que la portée d’exécution réellement observée.

Essayez vous-même

Accepted=9 et delivered=5. Le compteur FIFO vaut deux et les deux étages sont valides. Le bilan est-il cohérent ? Si une autre entrée est acceptée sans livraison et que l’occupation reste quatre, que s’est-il probablement passé ?

Lire l’explication

Le bilan correspond : 9-5=2+1+1=4. Après une autre acceptation sans livraison, la différence devient cinq. Une occupation de quatre suggère une admission sans capacité ou un élément écrasé. Examinez la disponibilité au premier front défaillant.