Die formale Verifikation gilt als eines der zuverlässigsten Mittel, um Designfehler frühzeitig aufzudecken, scheitert in der Praxis aber oft an der aufwendigen manuellen Erstellung von Properties. Ingenieure müssen Spezifikationen, die häufig in natürlicher Sprache oder als Dokumentprosa vorliegen, in exakte formale Aussagen übersetzen, die sich mit Tools wie SVA-Assertions prüfen lassen. Genau hier setzen aktuelle Untersuchungen an, ob Large Language Models diesen Übersetzungsschritt zumindest teilweise automatisieren können.

Erste Ergebnisse zeigen, dass LLMs durchaus in der Lage sind, aus strukturierten Spezifikationstexten sinnvolle Property-Entwürfe abzuleiten, insbesondere wenn die Eingabetexte bereits eine gewisse technische Präzision und Konsistenz aufweisen. Problematisch bleibt jedoch der Umgang mit Mehrdeutigkeiten, impliziten Annahmen und domänenspezifischem Kontext, der in realen Spezifikationsdokumenten häufig nur unvollständig explizit gemacht wird. Die generierten Properties müssen daher weiterhin von erfahrenen Verifikationsingenieuren überprüft werden, bevor sie produktiv eingesetzt werden können.

Grenzen und Chancen im Verifikationsablauf

Ein zentrales Problem ist die Bewertung der Korrektheit der generierten Properties selbst: Ohne eine verlässliche Ground Truth ist es schwierig zu beurteilen, ob eine vom Modell erzeugte Aussage tatsächlich die Designabsicht korrekt abbildet oder lediglich plausibel klingt. Dennoch sehen viele Beobachter in diesem Ansatz einen vielversprechenden Weg, um den Einstieg in die formale Verifikation zu erleichtern und die Erstellung von Testbenches sowie Assertions zu beschleunigen, auch wenn menschliche Kontrolle vorerst unverzichtbar bleibt.

Insgesamt deutet sich an, dass LLM-gestützte Werkzeuge künftig als Assistenzsysteme in Verifikationsteams Einzug halten könnten, ohne jedoch die fachliche Expertise vollständig zu ersetzen. Die Kombination aus automatisierter Vorschlagserstellung und gezielter menschlicher Nachprüfung könnte den Verifikationsprozess effizienter gestalten, ohne die Zuverlässigkeit formaler Methoden zu gefährden.