Vom Smartphone bis zum KI-Rechenzentrum: Moderne Chips müssen fehlerfrei funktionieren. Im Projekt OverSemi wurde eine Software zur mathematischen Verifikation von Chip-Designs entscheidend weiterentwickelt. Sie weist bereits während der Entwicklung nach, dass Optimierungen die vorgesehene Funktion des Chips nicht verändern werden – und hilft so, kostspielige Fehler frühzeitig zu vermeiden.

EIC-Accelerator-Projekt: OverSemi

„Optimisation of a novel software tool for automation of the design & verification process of semiconductor development“

Wenn klassische Prüfmethoden an ihre Grenzen stoßen

Die Komplexität moderner Chips wächst schneller, als klassische Prüfmethoden Schritt halten können. Früher war die formale Verifikation – also der mathematische Nachweis, dass ein Chip-Design korrekt funktioniert – ein einzelner technischer Zwischenschritt. Inzwischen hat wegen der großen Komplexität die Zahl der zu prüfenden Zustände sehr stark zugenommen. Damit ist die formale Verifikation zu einem strategischen Engpass geworden. Und wenn ein Fehler unentdeckt bleibt, kann er bis in die Serienfertigung gelangen und hohe Kosten verursachen.

Hier setzt das EIC-Accelerator-Projekt OverSemi an. Die zentrale Innovation besteht darin, einen mathematischen Verifikationsansatz so auszubauen, dass ein einmal erbrachter Korrektheitsnachweis auch nach späteren Optimierungen des Chip-Designs erhalten bleibt. So lässt sich belegen, dass Anpassungen – etwa zur Steigerung der Leistung, Verringerung des Flächenbedarfs oder Senkung des Energieverbrauchs – die spezifizierte Funktion des Chips nicht verändern. Die LUBIS EDA GmbH aus Kaiserslautern baute dafür ein bereits intern genutztes Software-Werkzeug gezielt aus. Im Mittelpunkt stand die Überführung des bestehenden Verifikationsansatzes in eine praxistaugliche Software.

Damit adressiert das Projekt ein weiteres Problem: den Fachkräftemangel. Bislang hängt die formale Verifikation stark vom Erfahrungswissen weniger Expertinnen und Experten ab – Wissen, das bisher kaum systematisch dokumentiert oder verfügbar gemacht wurde. Ziel von OverSemi war es daher, dieses Expertenwissen schrittweise in Software abzubilden und damit einer breiteren Nutzergruppe zugänglich zu machen, etwa auch Berufseinsteigerinnen und Berufseinsteigern. Dazu wurde das Werkzeug plattformunabhängig nutzbar gemacht, benutzerfreundlicher gestaltet und erstmals gemeinsam mit Industrie- und Forschungspartnern erprobt.

Die Technologie hinter OverSemi

Kurz gesagt: OverSemi ermöglicht es, bereits während der Chipentwicklung mathematisch nachzuweisen, dass ein Chip wie vorgesehen funktioniert – auch dann, wenn er später technisch optimiert wird. Das im Projekt entwickelte Software-Werkzeug basiert auf dem formalen Verfahren Path-Predicate-Abstraction (PPA). Dabei wird mathematisch überprüft, ob die detaillierte technische Beschreibung eines Chips auf Register-Transfer-Ebene (RTL – Register Transfer Level) genau dem zuvor entwickelten Funktionsmodell entspricht. So lässt sich bereits während der Entwicklung nachweisen, dass der Chip später wie vorgesehen arbeiten wird.

Die technische Herausforderung bestand darin, diese Korrektheitsgarantie auch dann aufrechtzuerhalten, wenn während der Implementierung praxisübliche Optimierungen vorgenommen werden. Dazu zählen beispielsweise die Reduzierung von Redundanzen, die Optimierung von Registern, internes Pipelining oder energieeffiziente Codierungen wie Gray-Code. Im Projekt wurde für jeden dieser Optimierungsschritte ein formaler Nachweis entwickelt, sodass die Übereinstimmung mit dem ursprünglichen Modell trotz der Änderungen erhalten bleibt.

Um die Integration in bestehende Entwicklungsprozesse zu erleichtern, wurde das Werkzeug um die Unterstützung gängiger Beschreibungs- und Verifikationssprachen erweitert. Es verarbeitet unter anderem SystemC/TLM, SystemVerilog und Python als Eingabe und erzeugt Verilog sowie SystemVerilog Assertions (SVA) für die weitere Verifikation. Ergänzend wurden eine mehrsprachige Benutzeroberfläche sowie eine höhere Toleranz gegenüber unterschiedlichen Eingabestilen umgesetzt, um den Einsatz des Werkzeugs für verschiedene Nutzergruppen zu vereinfachen. Dadurch lässt sich der formale Verifikationsansatz leichter in bestehende industrielle Entwicklungsumgebungen integrieren.

Nutzen für die Halbleiterentwicklung

Von der weiterentwickelten Software profitieren insbesondere Unternehmen und Entwicklungsteams, die digitale Halbleiter-IP auf RTL-Ebene entwickeln. Sie können die funktionale Korrektheit ihrer Chip-Designs bereits früh im Entwicklungsprozess mathematisch nachweisen und dadurch kostspielige Fehler in späteren Entwicklungsphasen vermeiden.

Da sich das Werkzeug in bestehende Entwicklungsumgebungen integrieren lässt, können Entwicklungsteams die Erstellung und Aktualisierung ihrer Verifikationsumgebung stärker automatisieren. Das reduziert den Aufwand nach Designänderungen, verkürzt Debug-Schleifen und schafft mehr Zeit für anspruchsvolle Verifikationsaufgaben.

Die erste Erprobung mit Industrie- und Forschungspartnern verlief vielversprechend. Eine belastbare Aussage zur wirtschaftlichen Wirkung ist derzeit jedoch noch nicht möglich, da die Marktvalidierung noch andauert.

Von der Forschung in die Anwendung

Technisch besonders anspruchsvoll war es, die mathematischen Korrektheitsnachweise auch nach Optimierungen am Chip-Design zuverlässig aufrechtzuerhalten.

Eine weitere große Herausforderung war, das bisher intern genutzte Expertenwerkzeug so weiterzuentwickeln, dass es auch von weniger erfahrenen Anwenderinnen und Anwendern effizient genutzt werden kann. Dafür wurde die Benutzeroberfläche überarbeitet und das Werkzeug gemeinsam mit externen Partnern erprobt. Gleichzeitig wurde das Werkzeug so weiterentwickelt, dass es plattformunabhängig auf Windows, Linux und macOS eingesetzt und über eine containerbasierte Architektur problemlos in bestehende Entwicklungsumgebungen integriert werden kann.

Ausblick

Nach einer erfolgreichen ersten Erprobung mit Industrie- und Forschungspartnern wird das Werkzeug derzeit in weiteren Anwendungsszenarien getestet. Langfristig möchte die LUBIS EDA GmbH ihr über viele Jahre aufgebautes Expertenwissen zur formalen Verifikation schrittweise in Software überführen und sich damit vom spezialisierten Dienstleister zu einem Software-Anbieter weiterentwickeln.

Tipps für die Antragstellung im EIC Accelerator

• Aus Sicht der LUBIS EDA GmbH sollten Antragstellende die Vorbereitung auf den Pitch nicht unterschätzen, realistische, nicht zu ambitionierte Meilensteine planen und von Beginn an ausreichend Spielraum für Anpassungen im Projektverlauf einplanen – beispielsweise bei der Ressourcenplanung.
• Hilfreich war zudem ein frühzeitiger und offener Austausch mit dem Project Officer (PO), um mögliche Abweichungen im Projektverlauf gemeinsam zu besprechen und Lösungen zu entwickeln.

Projektinfos im Überblick

• Projekt: OverSemi („Optimisation of a novel software tool for automation of the design & verification process of semiconductor development“)
• Förderprogramm: EIC Accelerator – Grant first (Horizon Europe) 
• Laufzeit: Januar 2024 bis Dezember 2025
• Fördersumme: 2,49 Mio. EUR
• Innovation: Software zur Optimierung der formalen, mathematisch abgesicherten Verifikation von Chip-Designs
• Zielgruppe: Unternehmen und Forschungseinrichtungen im Bereich der digitalen Halbleiterentwicklung
• Unternehmen: LUBIS EDA GmbH, Kaiserslautern
• Website: www.lubis-eda.com
• Kontakt: contact@lubis-eda.com