Formale Analyse prüft IC-Verbindungen in Minuten

Die heterogene Integration mehrerer ICs in einem einzigen Gehäuse zusammen mit einem leistungsfähigen Speicher mit hoher Bandbreite ist für viele Hochleistungs-Rechenanwendungen von entscheidender Bedeutung. Derartige Gehäusedesigns weisen eine hochkomplexe Konnektivität mit vielen hunderttausenden Verbindungen auf, was die Überprüfung der einzelnen Verbindungen äußerst schwierig macht. Das herkömmliche Verfahren erfordert viel Arbeitsaufwand und Zeit und ist entweder nicht umfassend oder findet zu spät im Prozess statt, da es in der Regel erst nach Abschluss der Implementierung durchgeführt wird.

Die Komplexität erfordert eine Shift-Left-Strategie

Elektronik-Entwicklung

Das sind die Herausforderungen der 3D-IC-Multiphysik

Angesichts der Komplexität von 3D-ICs sprechen sich Experten für einen „Shift-Left“-Ansatz aus. Dieser stellt die frühzeitige Designoptimierung und Simulation in den Fokus, um so die Herausforderungen der Multiphysik zu bewältigen. Proaktive Strategien sind entscheidend für die Überwindung von Hindernissen bei Halbleitertechnologien der nächsten Generation.Angesichts der Komplexität von 3D-ICs sprechen sich Experten für einen „Shift-Left“-Ansatz aus. Was es damit auf sich hat, erfahren Sie hier.

Wie funktioniert formale Verifikation bei IC-Gehäusen?

Eine Methode zur funktionalen Überprüfung der Konnektivität innerhalb eines Gehäuses kann mithilfe der formalen Verifikation alle Verbindungen zwischen IC-Blöcken umfassend überprüfen. Der Ablauf erfolgt für alle Schritte automatisch, von der Erstellung der Konnektivitäts-Spezifikationen bis zur Überprüfung der Konnektivität des Gehäuseausgangs. Die automatischen Parallelalgorithmen auf dem Rechnerverbund verifizieren eine Vielzahl von Verbindungen in Minuten oder sogar Sekunden. Das Skript für den Ablauf ist einfach und lässt sich in wenigen Minuten einrichten. Sobald es erstellt ist, kann es für verschiedene Gehäuse wiederverwendet werden.

Automatisierter Ablauf der Konnektivitätsprüfung

Formale Verifikationstools, die speziell auf die Konnektivitäts-Prüfung zugeschnitten sind, eignen sich gut, um die Verbindungen innerhalb von Gehäusen in frühen Prozessschritten zu überprüfen. Formale Konnektivitätslösungen erfordern von den Gehäusedesignern weder langwierige Testbenches und Assertionen für möglicherweise Millionen von Verbindungen, wie sie für eine Simulation erforderlich wären, noch ein Verständnis der Funktion des Designs oder des Ablaufs einer Simulation. Für die Überprüfung der Verbindungen zwischen mehreren Dies benötigen formale Tools keine Funktionsmodelle der Dies.

3D-IC-Design mit KI

Elektronik-Entwicklung

Siemens erweitert EDA-Portfolio für 3D-ICs

Siemens Digital Industries Software hat auf der DAC 2025 neue EDA-Lösungen für 3D-ICs vorgestellt. Im Fokus stehen eine modulare Tool-Suite für den Entwurf komplexer Chip-Architekturen sowie KI-gestützte Automatisierung im gesamten Designprozess.Hier erfahren Sie, welche neuen EDA Lösungen für 3D-ICs Siemens Digital Industries Software auf der DAC 2025 vorgestellt hat.

Sie brauchen nur zwei Dinge: Das Top-Modul des Systems, das die Dies instanziiert und die Verbindungsinformationen der Dies enthält und die Modul-Port-Definitionen der Dies, in der Regel die „Blackbox“-Module, die vom Designteam für Gehäuse empfangen werden

Die formale Verifikation eignet sich besonders für die Überprüfung der Verbindungen in Chiplets. Formale Methoden können in diesem Zusammenhang auf verschiedene Weise helfen.

Welche Schritte umfasst der Verifikationsprozess?

Eine formale Konnektivitätslösung erkennt Fehler bei Verbindungen innerhalb von Gehäusen. Sie kann das Ausgangsmodul des Gehäuses mathematisch anhand der Konnektivitäts-Spezifikation analysieren und Unstimmigkeiten oder Verstöße gegen die vorgesehenen Verbindungen identifizieren, die zu elektrischen Fehlern führen. Findet sie unterbrochene Verbindungen, liefert sie Signalverläufe, um das Problem anzuzeigen. Zudem verfügt sie über alle anderen erforderlichen Funktionen zur Fehlerbehebung.

• Korrekte Verbindungen sicherstellen: Da bei der formalen Verifikation eine umfassende mathematische Analyse unter Berücksichtigung aller möglichen Stimuli durchgeführt wird, kann überprüft werden, ob die Signale wie vorgesehen übertragen werden. Dazu wird nachgewiesen, dass die Verbindungen den festgelegten Anforderungen entsprechen. Wenn eine Verbindung nachgewiesen wird, gibt es kein Szenario, das die Verbindung unterbrechen kann, d. h. es gibt keine übersehenen Szenarien.
• Kurzschlüsse vermeiden: Die formale Überprüfung kann potenzielle Kurzschlüsse oder andere Verbindungsprobleme im Gehäuse erkennen, indem sie unbeabsichtigte Verbindungspfade aufdeckt.
• Komplexe Systeme mit millionenfachen Verbindungen: Der formale Ablauf generiert automatisch eine goldene Verbindungsspezifikation – ohne dass manuell CSV-Dateien von Verbindungen erstellt werden müssen – und kann eine große Anzahl von Verbindungen mithilfe paralleler Algorithmen überprüfen.
• Früherkennung: Die formale Verifikation kann direkt nach dem Prototyping des Gehäuses vor dessen physischer Implementierung durchgeführt werden. Etwaige Fehler in der Planungs- und Prototypenphase lassen sich frühzeitig erkennen, was viel Zeit und Geld spart.
• Sicher und zuverlässig: Nur eine formale Verifikation kann eine umfassende Analyse durchführen. Für Branchen wie die Luft- und Raumfahrt, die Automobilindustrie und die Medizintechnik ist die formale Verifikation zur Überprüfung der Korrektheit der Verbindungen in IC-Gehäusen von entscheidender Bedeutung.
• Compliance: Formale Werkzeuge sollten nach ISO 26262 zertifiziert sein, was für Audits und die Qualitätskontrolle in Branchen mit strengen regulatorischen Standards unerlässlich ist.

Wie lässt sich die Verbindungsspezifikation generieren?

Wenn formale Tools verwendet werden, um die Verbindungen nach der Prototypenentwicklung des Gehäuses zu überprüfen, benötigen Designer die Spezifikation der Verbindungen. Einige Unternehmen erstellen diese Spezifikation manuell in CSV-Dateien und schreiben Skripte, um das Top-Modul des Systems zu erzeugen und die Dies gemäß den Verbindungsspezifikationen zu instanziieren. In diesem Fall kann die vorhandene CSV-Datei als Spezifikation zur Überprüfung der Ausgabedateien des Gehäuses verwendet werden. Wenn keine CSV-Spezifikation der Verbindungen vorhanden ist, erstellen die Designer die Verbindungsspezifikation entweder manuell in einem Format, das vom formalen Werkzeug akzeptiert wird, oder sie verwenden ein Konnektivitätsextraktionstool, um die Spezifikation zu generieren, wenn das Design- oder Verifikationsteam das Top-Modul des Systems bereits erstellt und eine Funktionsprüfung durchgeführt hat. Die Designer können das Top-Modul und die Blackboxes der Dies als goldenes Referenzmodell verwenden und deren Verbindungen als Spezifikation.

Wenn die Designer über die Spezifikationen der Verbindungen und die Ausgabenetzlistendatei aus dem Gehäuse-Tool verfügen, können sie das formale Konnektivitätstool ausführen, um zu überprüfen, ob das Ausgabedesign des Gehäuses die Verbindungsspezifikationen erfüllt.

Zwei Testszenarien

In den beiden Testszenarien wurde der in Bild 2 dargestellte Ablauf verwendet. Zunächst wurden mit Hilfe von goldenen Referenzmodellen und dem Siemens EDA-Tool Connectivity Explorer die Verbindungen automatisch aus dem Referenzmodell extrahiert und in eine CSV-Datei exportiert. Anschließend wurden die Verilog-Netzlisten mithilfe des Tools Xpedition Substrate Integrator (xSI) generiert. Schließlich kam das formale Tool Check Connect zum Einsatz, um automatisch Prüfungen für die Verbindungen in der CSV-Datei zu generieren und formal zu überprüfen, ob die Ausgabedatei des Gehäuses den Verbindungen in der CSV-Spezifikationsdatei entspricht, d. h. um zu sehen, ob der Packaging-Prozess Verbindungen im goldenen Referenzmodell unterbrochen hat.

Bei der Verwendung formaler Konnektivitätslösungen ist das Skript sehr einfach und die Erstellung dauert nur wenige Minuten. Nach Fertigstellung des Skripts erfolgt die Ausführung automatisch. Bei der Verwendung des formalen Tools zur Überprüfung von Gehäuseverbindungen sind nur die Verbindungen zwischen den Blöcken von Interesse. Die Designer müssen nichts über die Funktionalität innerhalb der einzelnen Blöcke wissen. Das Package-Tool kann Module ohne interne Logik exportieren und behält nur die Ports und Verbindungen zwischen den Blöcken bei.

LinkedInReihe von Sandra Paggen-Breu

Elektronik-Fertigung

Kurz erklärt: Begriffe der Elektronikfertigung

TG130, HASL, Fine Pitch, Rework und NanoWiring. Dies ist nur ein Bruchteil der Begriffe, die in der Elektronikfertigung kursieren. Aber was versteckt sich dahinter?Hier finden Sie einen Überblick über Begriffe aus der Elektronikfertigung und was dahinter steckt.

Die Designteams für Gehäuse erhalten oft nur das Top-Modul des Systems und die Blackbox der Dies von den Systemverifikationsteams. Selbst wenn die Gehäuseteams die vollständigen Funktionsmodule vom Systemverifizierungsteam für das goldene Referenzmodell erhalten, kann Connectivity Explorer die Die-Module als Blackboxes behandeln und die Verbindungen zwischen den Dies extrahieren. Durch das Blackboxing der Die-Module kann das formale Tool bei jeder Systemgröße sehr schnell laufen. Bei der Überprüfung des Gehäusedesigns anhand der CSV-Verbindungsspezifikation läuft Check Connect ebenfalls schnell und kann große Systeme mit vielen Dies verarbeiten, da nicht viele sequenzielle Logiken zu analysieren sind.

Debugging-Funktionen bei Verbindungsfehlern

Wenn Check Connect für das Gehäusedesign mit der CSV-Verbindungsspezifikation ausgeführt wird und das Tool alle Verbindungen vollständig nachweist, können die Designer sicher sein, dass das Gehäusedesign die Verbindungsspezifikation erfüllt. Stellt das Tool Verstöße fest, wissen sie, dass im Design einige Verbindungen unterbrochen und Signale in falsche Pfade geleitet wurden.

Stellt das Tool einen Verstoß fest, wird ein kurzes Gegenbeispiel im „Wave Tab“ angezeigt, um die Unstimmigkeit in der Verbindung zu verdeutlichen. Mit den Signalverläufen und den umfangreichen Debugging-Funktionen, wie Source Tracing und der schematischen Ansicht, die das formale Tool bereitstellt, lässt sich die Ursache des Problems leicht finden.

Besteht die Möglichkeit, dass das Referenzmodell oder die Verbindungsspezifikation einige Verbindungen übersehen hat? Dies ist nicht auszuschließen, da die Systemfunktionsprüfung eventuell nicht vollständig ist oder die Gehäuseplanung vor Abschluss der Systemfunktionsprüfung begonnen wird. Können durch das Gehäusedesign ungewollt weitere Pins oder Verbindungen entstehen? Diese Situation ist selten. Es mag vereinzelt zu Fehlern kommen, wenn z. B. aufgrund von Tippfehlern neue Pins hinzugefügt werden.

Eine Lösung für dieses Problem ist die Verwendung einer speziellen Funktion von Check Connect, mit der ein Bericht über fehlende Anschlüsse erstellt werden kann. Darin sind die Ports des Top-Moduls und die Dies aufgelistet, für die keine Verbindung besteht. Wenn es einen Port gibt, der von der Anschlussspezifikation nicht abgedeckt ist, muss zunächst geprüft werden, ob die Portdefinition im Gehäusedesign korrekt ist und kein Fehler vorliegt. Ist die Portdefinition korrekt, liegt das Problem entweder im Referenzmodell, aus dem die CSV-Datei extrahiert wird, oder in der ursprünglich manuell erstellten Verbindungsspezifikation. Bei fehlenden Verbindungsdefinitionen können diese manuell hinzugefügt und Check Connect für das Gehäusedesign erneut ausgeführt werden. (bs)