Homepage Sitemap Contact




Home « Studies « Teaching Materials
Sorry, only available in german.


Funktionsdarstellung in der formalen Verifikation (03-701.20)

Um die Realisierung einer Schaltung gegen ihre Spezifikation zu verifizieren, wird ein Äquivalenztest der repräsentierten Booleschen Funktionen durchgeführt. Durch Desicion Diagrams (DD) lassen sich Boolesche Funktionen als gerichtete azyklische Graphen darstellen. Insbesondere sind Binary DDs (BDD) zur Darstellung von Funktionen in der Verifikation von integrierten Schaltungen etabliert, da der Äquivalenztest in konstanter Zeit möglich ist, sobald die BDDs der Funktionen aufgebaut sind. Verschiedene Varianten von BDDs, die sich zur Darstellung bestimmter Funktionenklassen eignen, werden verwendet. Durch allgemeinere Typen von DDs können auch nicht Boolesche Funktionen dargestellt werden.

Es existieren effiziente Algorithmen für den Aufbau von DDs zu einer gegebenen Funktion bzw. Schaltung. Desweiteren werden verschiedene heuristische Minimierungsverfahren verwendet, um auch größere Schaltungen bearbeiten zu können. Bezüglich der Laufzeit bzw. Größe von DDs für bestimmte Typen von Schaltungen existieren nur zum Teil Abschätzungen. In der neueren Forschung ist der Zusammenhang von DDs und SAT-Problemen von großem Interesse, da sie als verschiedene Ansatzpunkte für das gleiche Problem verwendet werden und einander (hoffentlich) ergänzen können.

Das Seminar soll ausgehend von einer kurzen Einführung in den Bereich der formalen Verifikation über eine Übersicht der Typen von DDs zu den Kernpunkten der aktuellen Forschung führen.



 Entnehmen Sie Angaben bezügl. Ort und Zeit bitte der LV-Liste der Universität Bremen



[Folien (ausser Übungsblätter) nur aus dem Campusnetz erreichbar]




  Zur Liste der Lehrveranstaltungen der Universität Bremen




zurück





Deutsch








Sitemap Kontakt

ISMVL2014 DUHDE