Digitale Modellierung Asynchroner Integrierter Schaltungen

Der Projektantrag DMAC: Faithfully Modeling Asynchronous Digital Circuits for Fast Dynamic Timing Analysis and Formal Verification ist der Entwicklung eines rein digitalen Modells für asynchrone integrierte Schaltungen gewidmet, das eine genaue und schnelle dynamische Zeitanalyse erlaubt und auch eine notwendige Grundlage für jeden Versuch einer praktikablen formalen Verifikation derartiger Designs darstellt. Das gesuchte Modell soll genau und realistisch (= getreu) sein, in dem Sinn, daß das Verhalten der digital modellierten Schaltung im Rahmen der erreichbaren Genauigkeit exakt dem Verhalten des korrespondierenden realen Schaltung entsprechen muß. Im Gegensatz zu analogen Modellen, die in der Regel getreu sind, aber exzessiv lange Simulations- und Verifikationszeiten implizieren, ist unser Ziel ein zeitkontinuierliches aber wertdiskretes Modell, was auf ein elaborates Delay-Modell für Gates und/oder Verbindungskanäle hinausläuft. Die Projektidee wurde durch einigen Entdeckungen stimuliert, die im Kontext zweier kürzlich abgeschlossener FWF-Projekte gemacht wurden. In diesen Projekten wurde die Bedeutung der von DMAC abgedeckten wissenschaftlichen Fragestellungen aus zwei sehr unterschiedlichen Blickwinkeln erkannt: Als eine Basis für Korrektheitsbeweise für fehlertolerante digitale Schaltungen und als eine unvermeidbare Voraussetzung für jeglichen praktikablen Ansatz einer formalen Verifikation größerer asynchroner Designs. Bei unseren Versuchen, die zugrundeliegenden Probleme zu verstehen, sind wir mehr oder weniger zufällig auf Involution Channels gestoßen, deren Input-Output-Delay, in scharfem Kontrast zu fast allen existierenden Ansätzen, von der Vergangenheit abhängt und eine selbstinverse Funktion darstellt. In der Folge hat sich herausgestellt, daß Involution Channels der einzige bislang bekannte Ausgangspunkt für ein realistisches digitales Modell sind. DMAC ist der vollständigen wissenschaftlichen Erkundung und Aufbereitung diesen Ansatzes gewidmet. Die wichtigsten offenen Fragestellungen, die in diesem Projekt beantwortet werden sollen, sind: Wie kann die Klasse von Schaltungen, für die das Involution-Modell und mögliche Varianten getreu sind, erweitert werden? Wie können Gates mit unterschiedlichen elektrischen Eigenschaften zusammengeschaltet werden? Wie kann das Modell für verschiedene Technologien und Betriebsbedingungen parametrisiert und charakterisiert werden? Wie kann der Gültigkeits-/Anwendungsbereich des Modells und dessen Genauigkeit weiter gesteigert werden? Darüberhinaus ist geplant, die zu entwickelnden Modelle in existierende Zeitanalyse- und Verifikationswerkzeuge zu integrieren. Dies soll nicht nur die prinzipielle praktische Eignung unseres Ansatzes demonstrieren, sondern stellt auch einen unerläßlichen Schritt zur experimentellen Evaluation der Modellierungsgenauigkeit dar.

Das Projekt DMAC (Faithfully Modeling Asynchronous Digital Circuits for Fast Dynamic Timing Analysis and Formal Verification) war der Entwicklung rein digitaler Modelle für asynchrone integrierte Schaltungen gewidmet, die eine genaue und schnelle dynamische Zeitanalyse erlauben und auch eine notwendige Grundlage für jeden Versuch einer praktikablen formalen Verifikation derartiger Designs darstellen. Die gesuchten Modelle sollten genau und realistisch (= getreu) sein, in dem Sinn, daß das Verhalten der digital modellierten Schaltung im Rahmen der erreichbaren Genauigkeit exakt dem Verhalten des korrespondierenden realen Schaltung entsprechen muß. Im Gegensatz zu analogen Modellen, die in der Regel getreu sind, aber exzessiv lange Simulations- und Verifikationszeiten implizieren, ist unser Ziel ein zeitkontinuierliches aber wertdiskretes Modell, was auf ein elaborates Delay-Modell für Gates und/oder Verbindungskanäle hinausläuft. Diese Projektziele wurden durch die Entwicklung und Analyse unseres Involution Delay Models und unserer Hybrid Thresholded Delay Models für Multi-Input Gates erreicht, und sogar in Form eines Prototyp-Tools für die schnelle dynamische Zeitanalyse digitaler integrierter Schaltungen implementiert.