Matthias Bernauer - Freiburg im Breisgau
      Start > Skript-Sammlung > Rechnerarchitektur > Verifikation >>







Verifikation



  • Validierung durch Simulation: Was geschieht bei der Verifikation durch Simulation?

    Eingangsstimuli erzeugen,
    Ausgangssignale beobachten

    Nachteil: unvollst. bei großen Simulationen


  • Welche 3 Formen der formalen Verifikation gibt es?
    äquivalenzprüfung, Modellprüfung, Theorembeweis

  • Wie funktioniert die äquivalenzprüfung bei kombinatorischen bzw. Sequentiellen Schaltungen?
    Die Frage ist, ob zwei gegebene digitale Schaltungen die gleiche Funktionalität haben. Bei kombinatorischen vergleichen wir die Ausgangssignale bei gleichen Eingangssignalen bei beiden Schaltungen | Bei sequentiellen Schaltungen: Sind die Ausgänge zu allen Zeitpunkten bei gleichen Eingabefolgen identisch. Das kann man überprüfen mit einem miter:

  • Formale Verifikation

    • äquivalenzprüfung: sind zwei Schaltungen äquivalent
      Was ist äquivalenzprüfung (Aeequivalence checking EC)?
      gegeben: zwei digitale Schaltungen
      gefragt: haben beide die gleiche Funktionalität (keine zeitliches Verhalten)
      bei kombinatorischen Schaltungen: sind die Ausgänge bei gleichen Eingangsbelegungen gleich?
      bei sequentiellen Schaltungen: sind die Ausgänge zu allen Zeitpunkten bei gleichen Eingabefolgen identisch?

      RTL
      Register
      Transfer
      Level


äquivalenzprüfung von Schaltkreisen: Problemverkleinerung durch
Zusammenfassung von strukturell gleichen Teilen: Schaltung 1 + 2
Vorgehen:
- Transformation der Schaltkreise in eine Normalformdarstellung (z.B. KNF, BDDs,...)
- Liegt äquivalenz der Normalformen vor? z.B. Sind BDDs gleich?
>> Alternative: Erzeuge miter-Schaltkreis (gelber Bereich)

Liefert der miter für alle Eingangsbelegungen 0, sind die Schaltungen äquivalent



-> es wurde eine übersetzung in ein Erfüllbarkeitsproblem vorgenommen.
Optimierungen: BDDs, SAT-Solver, Ausnutzen struktureller ähnlichkeiten, inkrementelle Verfahr.
Sat-Solver: Algorithmus zur Lösung von Erfüllbarkeitsproblemen (in KNF gegeben)

äquivalenzprüfung von Schaltwerken:
Schaltungen in Huffman-Normalform bringen, wenn gleiche Zustandskodierung und gleicher Startzu-
stand vorliegen, dann kann man das Problem auf die äqu.-prüfung von Schaltkreisen reduzieren.
Was ist, wenn man keine gleiche Zustandskodierung oder gemeinsamen Startzustand hat?
⇒ Einsatz von Techniken und Methoden der Automatentheorie
- Produktautomaten bilden mit miter-Ausgang
- Durchsuchen des Zustandsraumes nach erreichbaren Zuständen,
die „Unterschied“ am Ausgang erzeugen
-Symbolische Methoden mit BDDs


Def.: M = (I, O, S, s0, , ) ist Mealy-Automat gdw.:
- I endlich, nichtleere Menge von Eingabesymbolen ist
- O endlich, nichtleere Menge von Ausgabesymbolen ist
- S endlich, nichtleere Menge von Zuständen ist
- s0 aus S Anfangszustand ist
- : SxI -> S übergangsfunktion ist
- l: SxI -> O Ausgabefunktion ist

Berechnung eines Mealy-Automaten:
Sei w=(w0,w1,...) eine (un)endl. Folge von Eingabesymbolen
M = (I, O, S, s0, , ) berechnet eine (un)endl. Folge von Ausgabesymbolen u=(u0,u1,...) zu w
gdw. Es eine Folge von Zuständen s=(s0,s1,...) gibt, so dass
s0 = s; d(si,wi) = si+1; (si,wi) = ui für alle i >= 0

Def. Automatenäquivalenz:
Seien MA = (I, O, SA, s0A, A, A) und MB = (I, O, SB, s0B, B, B) Mealy-Automaten.
MA und MB heißen äquivalent gdw. MA und MB zu jeder Eingabefolge die identische Ausgabe-
folge berechnen. Prinzipiell kann die äqu. der Automaten folgendermaßen entschieden werden:
- Berechene zu MA und MB die minimalen Automaten MA,min und MB,min
- MA und MB sind äquivalent, wenn MA,min und MB,min bis auf Isomorphie identisch sind (info3)

Aber: Heutige Verfahren zur Automatenminimierung arbeiten auf den Zustandsgrafen von
MA und MB. Zustandsgrafen sequentieller Schaltungen können sehr groß werden, z.B. n FlipFlops führen zu 2n Zuständen. -> Alernativverfahren nutzen, bei denen eine explizite Repräsentation des Zustandsgrafen vermieden werden kann (symbolische Darstellung von Zustandsmengen mit BDDs)



Google MSN Suche
<< Start | Studium | Poolmgr | Tanzen | GPG | Impressum >>
Matthias Bernauer