Alexander Jesser: Mixed-Signal Circuit Verification Using Symbolic Model Checking Techniques

Zusammenfassung

Aufgrund der stetig steigenden Komplexität heutiger elektronischer Schaltungen können funktionale Fehler in diesen Systemen kaum noch ausgeschlossen werden. Mit den bisherigen Validierungsmethoden, wie z.B. dem Simulieren oder dem Testen, ist eine vollständige Überprüfung der Fehlerfreiheit aufgrund der Systemgrößen nicht mehr möglich. Die formale Verifikation hat sich zum Ziel gesetzt, funktionale Fehler bereits während der Designphase zu detektieren und vollständige Korrektheitsaussagen zu treffen. Model-Checking ist eine Klasse formaler Beweistechniken, die dem Modell eines Systems eine Menge formaler Spezifikationen gegenüberstellt und die totale Übereinstimmung beider überprüft.

Die Mixed-Signal-Schaltungen stellen eine in den letzten Jahren an Bedeutung gewonnene Schaltungsklasse dar. Die Integration von analogen und digitalen Schaltungsteilen auf einem monolithischen IC verspricht viele Vorteile, die bereits heute den Entwurf elektronischer Systeme revolutioniert.

Ausgehend von dieser Problemstellung werden in diesem Vortrag zwei symbolische Model-Checking Verfahren für Mixed-Signal Schaltungen vorgestellt.