Formal Abstraction and Verification of Analog Circuits (faveAC)

Das Projekt faveAC ist ein Projekt das von der Deutsche Forschungsgemeinschaft (DFG) gefördert wird. Dieses Projekt stellt eine Kooperationsarbeit zwischen der Leibniz Universität Hannover, Technische Universität München und der Gothe-Universität Frankfurt da.

Das Projekt befasst sich mit der Formalen Verifikation von AMS(Anlog-mixed-signal) Schaltungen. Im Vergleich zur der Digitalen Domäne ist die Verifikation in der Analogen Domäne schwach verbreitet. Ansätze für die Verifikation von analogen Schaltung sind nicht skalierbar und die, die es sind, befassen sich mit rein linearem verhalten. Allerdings ist das nichtlineare Verhalten einer Schaltung meist der Grund für das Versagen.

Die Universität Frankfurt erforscht an einer voll automatisierte Softwarelösung die durch Abstraktionen das Systemverhalten modelliert. Dabei sollen die getroffenen Abstraktionen weiterhin das komplette Systemverhalten beschrieben. Durch kompositionelle Methoden sollen die entwickelten Teilsysteme anschließend zusammengebracht werden. Ziel ist es einen Ansatz zu entwickeln der sowohl skalierbar als auch für nichtlineare Schaltungen anwendbar ist und somit die Verifikation von größeren AMS Schaltungen ermöglicht.

Um die getroffenen Abstraktionen abzusichern stehen Äquivalenzvergleichsmethoden der Abstraktionsebenen im Focus. Ein weiteres Ziel ist es Parameterschwankungen ebenfalls sicher einschließend mit zu modellieren. Der Ansatz ist kompositional, so dass größerer Systeme geprüft werden können. Abschließend wird die Verifikation der Schaltung mittels einer Erreichbarkeitsanalyse des abstrahierte Systemverhalten gegenüber den Anforderungen ermittelt.