Verifikation von Zeitbedingungen analoger Schaltungen durch Model-Checking-Verfahren

Inhalt:
In diesem Beitrag präsentieren wir Algorithmen zum Model-Checking analoger Schaltungen unter Berücksichtigung von Zeitbedingungen und eine Methodik, wie diese zur Verifikation von zeitbasierten Spezifikationskriterien eingesetzt werden können. Dazu wurde ein bekanntes Verfahren zum Model-Checking integrierter analoger Schaltungen um die Berücksichtigung von Zeitverhalten erweitert. Anhand von zwei beispielhaften Schaltungen wird das Verfahren erläutert und ein Vergleich mit der herkömmlichen Verifikation durch Schaltungssimulation gezogen.