26 / 37 · Konzept

Zähler debuggen und Gegenbeispiele minimieren

Kurze Tests entwerfen, die Reset-, Enable- und Umlauffehler unterscheiden.

Ein richtiger Endwert kann eine falsche Folge verbergen

Ein abschließender Zählerwert 0 beweist weder Reset noch Umlauf: Ein stets bei 0 stehender Zähler liefert dasselbe. Beobachtungspunkte müssen Inkrementieren, Halten, Reset^{Reset Steuerung zur Rückkehr in einen festgelegten Anfangszustand. Synchron/asynchron und Priorität gegenüber anderen Steuerungen müssen definiert werden. Mehr erfahren} und Grenzumlauf getrennt sichtbar machen.

Funktionen bewusst gleichzeitig aktivieren

Situation	Zu prüfende Anforderung
reset=1, enable=0	Wird reset durch enable verdeckt?
reset=1, enable=1	Hat reset Vorrang vor Inkrementieren?
count=M-1, enable=0	Kein falscher Umlauf im Halt
count=M-1, enable=1	Genau von M−1 nach 0
Resetwechsel zwischen Flanken	Synchroner Reset wirkt erst an der nächsten Flanke

Einzeln aktivierte Steuerungen decken Prioritätsfehler nur schlecht auf.

Jede Spalte dokumentiert eine steigende Flanke^{Steigende Flanke Übergang des Takts von 0 auf 1. Nicht zu verwechseln mit dem gesamten hohen Pegelintervall CLK=1. Mehr erfahren}. Eingänge gelten unmittelbar davor, Zustände mit „after“ unmittelbar nach der Aktualisierung. Die Spalten zeigen die Reihenfolge der Abtastungen, keine physische Laufzeit^{Laufzeit Zeit nach einer Eingangsänderung, bis der Ausgang auf dem richtigen Wert stabil ist. Logische Äquivalenz und zeitliche Eigenschaften sind getrennte Aussagen. Mehr erfahren}. Anfangs count=5. Der fehlerhafte Entwurf prüft reset nur innerhalb von enable und hält deshalb zuerst 5. Trotz gleichem Endwert deckt die erste Abweichung den Fehler auf.

Minimales Gegenbeispiel: enable verdeckt reset

Wellenformdaten anzeigen

Wellenformdaten: Jedes Zeichen steht für ein Intervall, ein Punkt hält den vorherigen Zustand und p ist ein Taktzyklus.
Signal	Wellenform	Buswerte
edge	`234`	E0 → E1 → E2
reset	`101`
enable	`01.`
correct after	`234`	0 → 1 → 0
bug after	`234`	5 → 6 → 0

Starten Sie die Modulo-8-Referenz bei 101. Wählen Sie enable=0, reset=1 und takten Sie: Korrekt ist 000. Falsches RTL mit reset innerhalb von enable hält 101. Prüfen Sie nach Resetfreigabe auch Halten bei enable=0 und Zählen bei enable=1 getrennt.

reset und enable gleichzeitig aktivieren

Der synchrone reset hat Vorrang vor enable. Bei enable=0 bleibt der gespeicherte Wert erhalten. q=101; q_next = (q + 1) mod 8

Die erste Abweichung mit einem Referenzmodell finden

C_{k+1}=r_k?0:(e_k?((C_k+1)\bmod M):C_k)

Dieses Modell setzt gültige Zustände 0 bis M−1 voraus. Ungültige Zustände brauchen eine zusätzliche Wiederherstellungsregel. Berechnen und vergleichen Sie jede Flanke. Eingabe und Zustand vor der ersten Abweichung bilden den kleinsten Ausgangspunkt für die Fehlersuche.

Tritt der Fehler erst nach 1000 Zyklen auf, entfernen Sie unnötige Abschnitte, bis er in drei bis fünf Flanken reproduzierbar ist. Bewahren Sie dieses minimale Gegenbeispiel nach der RTL-Korrektur als Regressionstest auf. Prüfen Sie geänderte Spezifikation und Code getrennt, damit Entwurf und Test nicht gemeinsam auf dieselbe falsche Bedingung geändert werden.

Selbst ausprobieren

Fehlerhaftes RTL umschließt reset mit if(en) begin if(rst) ... end. Welche Anfangsbedingung und Eingabe zeigen dies am kürzesten?

Erklärung lesen

Starten Sie ungleich 0 und geben Sie eine steigende Flanke mit rst=1, en=0. Resetpriorität verlangt 0; der falsche Entwurf hält den alten Wert. Ein Start bei 0 würde den Fehler verbergen.