Symbolische Zeitanalyse asynchroner Schaltungen

Die moderne Gesellschaft ist auf den zuverlässigen Betrieb integrierter Schaltungen angewiesen. Integrierte Schaltungen sind jene miniaturisierten elektronischen Systeme, die u.a. auch in Mobiltelefonen, Computern, Fahrzeugen, Medizingeräten, Sensoren und Kommunikationsnetzen vorkommen. Damit Chips korrekt funktionieren, müssen Signale die richtigen Stellen in der richtigen Reihenfolge zum richtigen Zeitpunkt erreichen. Besonders schwierig ist dies bei Schaltungen ohne zentralen Takt. Bei solchen asynchronen Schaltungen ist das Timing selbst Teil der Berechnung. Schon kleinste Timingfehler können zu falschen Ergebnissen, Energieverlusten oder seltenen, schwer reproduzierbaren Ausfällen führen.
Ingenieur*innen nutzen zwei Werkzeugklassen: 1. Schnelle digitale Simulationen, die viele Fälle prüfen, reale Vorgänge im Chip aber vereinfachen und daher wichtige Effekte übersehen. 2. Sehr genaue analoge Simulationen, die der physikalischen Realität näherkommen, jedoch so langsam sind, dass mittelgroße Schaltungen nicht gründlich untersucht werden können.
So entsteht eine Lücke zwischen Geschwindigkeit und Genauigkeit. Das Projekt schafft die wissenschaftlichen Grundlagen für einen neuen Analyseansatz. Anders als nicht erschöpfende simulationsbasierte Validierungsmethoden, verfolgt es eine neuartige symbolische Timinganalyse, die das gesamte Spektrum möglichen Schaltungsverhaltens vollständig erfasst. Grundlage sind analytische Verzögerungsformeln, welche die physikalischen Eigenschaften von Gattern und Leitungen einschließlich ihrer Abhängigkeit von Übergangshistorie und wechselwirkenden Eingängen präzise modellieren. Durch die Verknüpfung dieser Ausdrücke entlang von Signalpfaden mithilfe eines Computeralgebrasystems wird die Timinganalyse zu einer symbolischen Rechenaufgabe: Numerische Timinginformationen der Simulation werden durch symbolische, über uninterpretierte Variablen ausgedrückte Informationen ersetzt. Die resultierenden analytischen Timingausdrücke erlauben den Einsatz mathematischer Offline-Analysetools, um kritische Timingsituationen zu identifizieren und kritische Abhängigkeiten etwa von Prozess-, Spannungs- und Temperaturbedingungen zu untersuchen.
Eine zentrale Herausforderung dieser symbolischen Timinganalyse ist ihre inhärente Komplexität, da die Zahl möglicher Reihenfolgen von Signalübergängen rasch wächst. Ein wesentlicher Teil des Projekts konzentriert sich daher auf Maßnahmen zur Komplexitätsreduktion, gestützt auf Ideen und Techniken des Automated Reasoning und der formalen Verifikation.
Zu den angestrebten Ergebnissen zählen neben den erforderlichen formal-mathematischen Grundlagen, ein Open-Source-Forschungsprototyp eines Analysewerkzeugs sowie dessen Anwendung auf relevante Benchmark-Schaltungen. Insgesamt eröffnet das Projekt ein neues gemeinsames Arbeitsfeld für Schaltungsentwurf und Automated Reasoning. Langfristig kann es dazu beitragen, Probleme früher zu erkennen, kostspielige Redesigns zu reduzieren und Chips zuverlässiger, schneller und energieeffizienter zu machen.