Ein Ansatz für die semi-formale Verifikation von Mixed-Signal-Schaltungen mit Hilfe von Bounded Model Checking

In dieser Arbeit wird ein Ansatz für die verifikationsgerechte Modellierung des Verhaltens der analogen Komponenten von Mixed-Signal-Schaltungsentwürfen vorgestellet. Ausgehend von der Beschreibung des analogen Verhaltens in Form von Differentialgleichungen wird ein zeit- und wertediskretes Modell des Analogteils einer Mixed-Signal-Schaltung erstellt, in dem auch die dynamischen Einschwingvorgänge repräsentiert sind. Dieses Modell ersetzt in der Zusammenschaltung von Analog- und Digitalteil das durch das Differentialgleichungssystem gegebene kontinuierliche Analogmodell. Die auf diese Weise erzeugte Repräsentation eines Mixed-Signal-Schaltungsentwurfs kann mit den bekannten Methoden der formalen digitalen Verifikation verifiziert werden.