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.