Large Language Models nähern sich der Umsetzung einer der lästigsten Aufgaben bei der Verifizierung von Chipdesigns: der Umwandlung natürlichsprachlicher Spezifikationen in eine Reihe formaler Eigenschaften, die zur Bewertung der Korrektheit einer RTL-Implementierung verwendet werden können. Interviews, die Brian Bailey für Semiconductor Engineering führte, zeigen, dass die aktuellen Werkzeuge einen nützlichen ersten Entwurf erzeugen können, aber noch weit davon entfernt sind, eine vollständige Menge zu erstellen, die ohne intensive technische Prüfung übernommen werden kann.
Die Bedeutung dieser Entwicklung liegt darin, dass das Verfassen von Eigenschaften seit Jahren einen Engpass bei der formalen Verifizierung darstellt. SystemVerilog-Eigenschaften, die bei ihrer Einbindung in eine Verifizierungsumgebung als Assertions bezeichnet werden, dienen dazu, logische und zeitliche Beziehungen zwischen Signalen zu beschreiben, etwa das Verhalten beim Zurücksetzen, Handshakes, One-Hot-Bedingungen und grundlegende Sicherheitsprüfungen. Wenn diese Eigenschaften vollständig und präzise sind, können sie verwendet werden, um das Verhalten einer RTL-Implementierung mit der Spezifikation zu vergleichen, ohne an die Art und Weise gebunden zu sein, in der das Design erstellt wurde.
Was können die Werkzeuge heute leisten?
Ein auf einem Large Language Model basierendes Werkzeug kann ein Spezifikationsdokument, einen Protokollstandard oder sogar Kommentare innerhalb von RTL lesen und anschließend einen Entwurf von SVA-Eigenschaften vorschlagen. Ashish Darbari, CEO von Axiomise, sagt, dass diese Anwendung besser umsetzbar ist, wenn die Spezifikationen auf stabilen Standards beruhen, die sich nicht häufig ändern. In diesem Fall reduziert das Werkzeug den wiederholten Anteil der Erstellung des ersten Codeentwurfs, anstatt den gesamten Verifizierungsprozess zu übernehmen.
Einige Ansätze versuchen, die Genauigkeit der Modelle durch die Erstellung eines Knowledge Graph zu verbessern, also eines Wissensgraphen, der Entitäten und ihre Beziehungen speichert. Die Knoten können ein Signal, ein Modul, eine Anforderung oder einen Anschluss umfassen, während die Kanten Beziehungen wie „steuert“, „setzt zurück“ und „reagiert auf“ beschreiben. Statt Textabschnitte abzurufen, die scheinbar mit der Anfrage zusammenhängen, kann das System auf konkrete Fakten und Verknüpfungen zurückgreifen. Dadurch verringert sich die Wahrscheinlichkeit, dass ein Signalname erfunden oder eine Beziehung zwischen Designkomponenten falsch verstanden wird. Die Quelle verweist in diesem Zusammenhang auf eine Arbeit mit dem Titel RAG-SVA in the Landscape of LLM-Based Assertion Generation von Cohen und Chibani.
Das Problem beginnt vor der künstlichen Intelligenz
Das Werkzeug kann nichts extrahieren, was nicht bereits geschrieben oder entschieden wurde. Ravindra Aneja, Director of Applications Engineering bei Synopsys, sagt, dass die ideale Spezifikation in den vergangenen drei Jahrzehnten nicht verfügbar gewesen sei. Häufig beginne die Entwicklung, bevor die Dokumentation vollständig ist, und in manchen Projekten gebe es überhaupt keine vollständige Spezifikation, insbesondere bei abgeleiteten Designs oder wenn sich die Anforderungen während der Arbeit ändern.
Dieses Problem betrifft nicht nur die Formulierung, sondern auch das Änderungsmanagement. Ein Marketingteam kann beispielsweise ein neues Merkmal hinzufügen oder eine bestehende Anforderung ändern, woraufhin das Design- und das Verifizierungsteam die Auswirkungen dieser Änderung bestimmen müssen. Abhi Kolpekwa, Senior Vice President und General Manager bei Siemens EDA, ist der Ansicht, dass die Umwandlung einer Spezifikation in Eigenschaften „Kontextintelligenz“ erfordert, die die Historie und den Kontext von Änderungen verfolgt, und nicht einen Agenten, der jedes Mal neuen Text erzeugt.
Die Gefahr falscher Sicherheit
Die größte Einschränkung des aktuellen Ansatzes besteht darin, dass eine Eigenschaft syntaktisch korrekt sein kann, sodass sie übersetzt wird und die Verifizierungswerkzeuge ihren Beweis erfolgreich führen, ohne jedoch tatsächlich das beabsichtigte Verhalten zu prüfen. Darbari warnt davor, dass eine schwache oder vacuous Eigenschaft leicht erfolgreich sein kann, weil sie viele Verhaltensweisen zulässt, das falsche Signal verwendet oder eine fehlende beziehungsweise übermäßig restriktive Vorbedingung enthält. Daher bedeutet ein „grüner Beweis“ nicht, dass das Design fehlerfrei ist: Der Beweis ist nicht stärker als die Eigenschaft, die bewiesen wurde.
Die Quelle ergänzt, dass Modelle bei struktureller und syntaktischer Abdeckung tendenziell besser abschneiden als beim Verständnis der architektonischen Absicht und des Grundes, aus dem eine Regel existiert. Deshalb kann eine ungenaue Interpretation der Spezifikation durch das Modell in ein formal wirkendes und strenges Fragment überführt werden, während es eine Lücke in den Anforderungen verbirgt. Wenn diese Lücke in Arbeiten wie FMEDA, Sicherheitsunterlagen oder Zulassungsnachweise im Zusammenhang mit ISO 26262 und ISO 21434 gelangt, kann sich ihre Wirkung weit über das ursprüngliche Verifizierungsprojekt hinaus erstrecken.
Auch die Trennung von Design und Verifizierung rückt in den Mittelpunkt. Kaye Mao, Leiterin des Produktdesigns bei Normal Computing, weist darauf hin, dass der Zugriff der Agenten auf Projektmaterialien eingeschränkt werden müsse, da die Verwendung des Designs selbst zur Generierung von Testfällen durch den Agenten die Unabhängigkeit des Verifizierungsprozesses beeinträchtigen könne.
Was ändert sich in der Praxis?
Künstliche Intelligenz kann die Zeit für die Erstellung erster Entwürfe laut Darbari von Tagen auf Minuten verkürzen, aber sie kann den anschließenden Arbeitsaufwand vervielfachen. Jede generierte Eigenschaft muss anhand der Spezifikation geprüft, hinsichtlich der Abdeckung analysiert, auf Vacuity getestet und auf ihre Beziehung zu den Designs vorhandenen Signalen überprüft werden; außerdem kann bei Fehlern eine Analyse der Signalverläufe erforderlich sein. Wenn sich die Anzahl der Eigenschaften verzehnfacht und der für jede einzelne erforderliche Prüfaufwand gleich bleibt, kann der Prüfaufwand den durch die schnelle Generierung erzielten Gewinn übersteigen.
Aus Sicht von certi.news besteht die tatsächliche Veränderung nicht darin, den Verifizierungsingenieur zu ersetzen, sondern den Schwerpunkt vom Verfassen der Eigenschaften auf ihre Bewertung und die Rückverfolgbarkeit ihrer Quelle zu verlagern. Darbari empfiehlt, generierte Eigenschaften als Entwürfe und nicht als freigegebene Ergebnisse zu behandeln und vor ihrer Aufnahme in die Regression Suite ein Prüf-Gate einzurichten. Außerdem sollte die Quelle jeder Eigenschaft dokumentiert werden – der Absatz der Spezifikation, die Anforderung oder das RTL-Element, aus dem sie hervorgegangen ist –, damit der Ingenieur die Übereinstimmung überprüfen kann.
Dieser Ansatz kann die Einstiegshürde für Verifizierungsingenieure senken, die Formal Verification einsetzen möchten, sagt Yaron Ilani, Verification Solutions Engineer bei Normal Computing. Damit ist die Frage nach dem Return on Investment jedoch nicht geklärt. Kaye Mao ist der Ansicht, dass die Zeit für die Prüfung der Agentenausgaben in die Kosten einbezogen werden müsse, während Arvind Srinivasan, Head of Solutions Engineering bei Normal Computing, darauf hinweist, dass die Skalierung nicht nur die Rechenleistung betrifft, sondern auch die Vollständigkeit der Daten und die Kosten der menschlichen Prüfung.
Das Fazit lautet, dass Large Language Models inzwischen in der Lage sind, den automatisierbaren und wiederkehrenden Teil der Formulierung von Eigenschaften zu beschleunigen. Die beiden Probleme der Vollständigkeit der Spezifikation und des Verständnisses der Designabsicht haben sie jedoch noch nicht gelöst. Der Wert dieser Werkzeuge wird weiterhin davon abhängen, dass ein Ingenieur vorhanden ist, der das Design versteht, und dass unabhängige Mechanismen zur Messung der Abdeckung sowie zur Erkennung leerer oder ungeeigneter Eigenschaften existieren – nicht von der Anzahl der Eigenschaften, die das Modell erzeugen kann.