12 / 37 · Konzept

MUX-Verifikation: Vollprüfung und Eigenschaften

Kombinatorische Eingabeabdeckung und Speicherverhalten getrennt prüfen und Gegenbeispiele minimieren.

Was gilt als korrekt?

Ein-Bit-Daten a, b und sel ergeben acht Kombinationen; hier ist Vollprüfung effizient. Für einen MUX^{Multiplexer Kombinatorische Schaltung, die gemäß Auswahlsignal einen Eingang zum Ausgang verbindet. Die Zuordnung von Auswahlbits und Eingangsnummern muss festgelegt sein. Mehr erfahren} mit Datenbreite W wären es einschließlich Auswahl $2^{2W+1}$ Fälle. Schon etwas größere Breiten brauchen andere Strategien.

Für jedes Ausgangsbit gilt:

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

Stimuli nach Fehlerart auswählen

Gesuchter Fehler	Geeignete Eingabe oder Beobachtung
a/b vertauscht	Verschiedene a, b mit sel=0 und 1 vergleichen
Bitreihenfolge umgekehrt	Walking-one mit genau einem gesetzten Bit
Stuck-at-Fehler	Nur Nullen, nur Einsen, alternierende Bits
Falsche Speicherflanke	Eingänge zwischen Flanken ändern und q-Halten prüfen
Fehler um einen Zyklus	Unterschiedliche Sollwerte auf aufeinanderfolgenden Flanken

Viele Tests allein sind keine gute Verifikation. Erklären Sie, welchen Fehler jeder Test aufdecken soll.

Der folgende Vergleich wählt ausschließlich a≠b. Jede Spalte ist ein Testvektor. Die falsche Auswahl liefert in allen vier Spalten das Gegenteil von expected.

Vier Kombinationen zum Finden einer invertierten Auswahl

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
a	`0.1.`
b	`1.0.`
sel	`0101`
expected	`01.0`
swapped bug	`10.1`

Referenzmodelle unabhängig implementieren

Kopierter DUT-Code kann denselben Fehler zweimal implementieren. Leiten Sie Erwartungen aus Wahrheitstabelle^{Wahrheitstabelle Vollständige Liste aller Eingangskombinationen mit jeweiligem Ausgang. Zeitliche Änderungen werden gesondert im Zeitdiagramm geprüft. Mehr erfahren} oder Indexauswahl ab und verfolgen Sie q als gesonderten Abtastzustand. Verkürzen Sie bei mismatch die Eingabefolge auf ein minimales weiterhin scheiterndes Beispiel und erklären Sie die Ursache.

Protokollieren Sie an jedem Beobachtungspunkt Istwert, Sollwert und Eingabe statt nur den Endzustand. So unterscheiden Sie „Simulation lief“ von „Spezifikation erfüllt“.

Selbst ausprobieren

Ein 8-Bit-MUX wurde nur mit a=0x00, b=0xFF für beide Auswahlwerte geprüft. Erkennt dies eine umgekehrte Ausgangsbitreihenfolge?

Erklärung lesen

Nein. 0x00 und 0xFF bleiben bei Umkehrung unverändert. Verwenden Sie positionsabhängige Muster wie 0x01, 0x02 und vergleichen Sie jedes Ausgangsbit.