💻 computer science

From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

Dit artikel presenteert ProofLoop, een tool-augmented AI-agent die via een iteratief proces met formele verificatietools (zoals JasperGold) en contextuele informatieverzameling automatisch correcte SystemVerilog Assertions (SVA) genereert op basis van natuurlijke taal.

Oorspronkelijke auteurs: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

Gepubliceerd 2026-04-28

📖 3 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een enorme, hypermoderne LEGO-stad probeert te bouwen. De stad is zo complex dat er duizenden kleine radartjes, lampjes en bewegende onderdelen in zitten. Om te zorgen dat de stad niet instort of dat de verkeerslichten niet tegelijk op groen springen, heb je een "controleur" nodig die overal regels voor schrijft (bijvoorbeeld: "Als de trein nadert, moet het hek altijd dicht zijn").

In de wereld van computerchips noemen we die regels SVA (SystemVerilog Assertions). Het probleem? Het schrijven van die regels is ontzettend moeilijk. Je moet niet alleen weten hoe de stad eruitziet, maar ook precies hoe elk klein radartje op welk moment draait.

Dit wetenschappelijke artikel presenteert ProofLoop, een slimme digitale assistent die dit werk overneemt.

De Analogie: De Super-Detective met een Magische Vergroter

Je kunt ProofLoop zien als een super-detective die een taak krijgt: "Zorg dat de stad veilig werkt." Maar in plaats van alleen maar een handleiding te lezen (wat vaak niet genoeg is), werkt deze detective in twee slimme fasen:

Fase A: De Verkenning (De Detective met de Vergroter)

Stel je voor dat de detective een enorme bouwtekening krijgt. In plaats van alles uit zijn hoofd te leren, heeft hij een setje magische gereedschappen:

De Semantische Zoeker: Een soort Google voor de bouwtekening. De detective vraagt: "Waar zitten alle deuren in dit gebouw?" en krijgt direct een lijstje.
De Structuur-Scanner (JasperGold): Dit is een röntgenapparaat. De detective kan hiermee door de muren kijken om te zien: "Welke stroomkabel zit er precies aan dit lampje vast?" of "Wat gebeurt er als de hoofdschakelaar omgaat?"

De detective "denkt" na, gebruikt een tool, ziet het resultaat, en besluit dan pas wat zijn volgende stap is. Hij werkt dus niet blindelings, maar leert terwijl hij onderzoekt.

Fase B: De Test en de Correctie (De Detective als Controleur)

Nu de detective weet hoe de stad werkt, schrijft hij de regels (de SVA's). Maar hij is niet bang om fouten te maken. Hij stuurt zijn regels naar een strenge examenmeester (de Solver).

De Test: De examenmeester checkt de regel. "Hé, deze regel klopt niet! Je zegt dat de trein stopt, maar volgens mijn berekeningen rijdt hij gewoon door!"
De Reparatie: In plaats van de hele regel weg te gooien, krijgt de detective de foutmelding terug. Hij zegt: "Ah, ik begrijp het, ik heb de verkeerde kabel aangegeven. Ik pas de regel even aan."
De Herhaling: Dit doet hij een paar keer totdat de regel perfect is en de examenmeester zegt: "Gevonden! Deze regel is 100% waterdicht."

Waarom is dit een doorbraak?

Vroeger probeerden we computers (zoals ChatGPT) gewoon de regels te laten schrijven door ze de handleiding te geven. Dat ging vaak mis omdat de computer de details van de "machine" niet echt begreep. Het was alsof je een kok vraagt een gerecht te maken zonder dat hij de keuken mag zien.

ProofLoop is anders omdat:

Hij mag de keuken in: Hij onderzoekt zelf de ingrediënten en de apparatuur.
Hij leert van zijn fouten: Hij krijgt direct te horen wanneer een regel niet werkt en repareert hem direct.

Het resultaat? De onderzoekers lieten zien dat ProofLoop veel vaker regels schrijft die écht kloppen en die technisch perfect werken, zelfs bij hele ingewikkelde digitale systemen. Het is alsof de detective niet alleen de regels schrijft, maar ook zelf de hele veiligheidsinspectie uitvoert!

Technische Samenvatting: ProofLoop – Bridging LLMs & Formal Representations for RTL Assertion Generation

Het Probleem

Het schrijven van SystemVerilog Assertions (SVA) is cruciaal voor de formele verificatie van digitale hardware, maar het is een arbeidsintensief proces dat diepgaande expertise vereist in zowel Register-Transfer Level (RTL) semantiek als temporele logica. Hoewel Large Language Models (LLMs) veelbelovend zijn voor het automatiseren van deze taak, kampen huidige benaderingen met drie fundamentele problemen:

Verkeerde signaalreferenties: LLM's hebben geen direct inzicht in de hardwarestructuur.
Gebrek aan context: Ze missen cruciale metadata zoals klokdomeinen, reset-gedrag en signalen-afhankelijkheden (fan-in/fan-out).
Gebrek aan formele garanties: Directe prompting leidt vaak tot syntactisch incorrecte of functioneel onjuiste assertions die niet voldoen aan de werkelijke hardware-intentie.

Methodologie: Het ProofLoop Framework

De auteurs introduceren ProofLoop, een "tool-augmented ReAct agent" die werkt via een solver-in-the-loop benadering. Het proces is onderverdeeld in drie hoofdfasen:

AST Indexing & Knowledge Base: De RTL-code wordt geparsed met een SystemVerilog-compiler om een Abstract Syntax Tree (AST) te genereren. Deze wordt opgedeeld in semantische blokken (interfaces, always-blocks, instanties, assignments) en opgeslagen in een vector-database voor Retrieval-Augmented Generation (RAG).
Fase A: Contextverzameling (Agentic Context Synthesis): De agent gebruikt een Thought $\rightarrow$ Action $\rightarrow$ Observation loop (ReAct). De agent besluit autonoom welke tools hij aanroept:
- Retrieval tools: Voor semantische zoekopdrachten in de vector-database.
- Structural analysis tools: Deze koppelen direct met de formele tool Cadence JasperGold om hardware-specifieke metadata te extraheren (zoals fan-in/fan-out en flip-flop eigenschappen) die niet direct uit de tekst af te leiden zijn.
Fase B: Generatie & Verificatie Loop (Solver-in-the-loop): De agent genereert SVA-code en stuurt deze naar JasperGold.
- Als de assertion faalt (door syntaxisfouten of logische fouten), krijgt de agent de foutmeldingen en counterexample traces terug.
- De agent voert vervolgens gerichte reparaties uit (bijv. het corrigeren van klokdomeinen of signaalnamen) in plaats van de code volledig opnieuw te genereren. Dit proces wordt tot maximaal drie rondes herhaald.

Belangrijkste Bijdragen

Agentic Context Synthesis: Een systeem dat niet alleen tekst zoekt, maar actief hardware-metadata opvraagt via een redeneerproces.
Solver-in-the-loop Refinement: Het integreren van formele feedback (JasperGold) om de kloof tussen natuurlijke taal en strikte logische specificaties te overbruggen.
Schaalbaarheid: Een methode die effectief blijft bij complexe, multi-module ontwerpen door gebruik te maken van modulaire AST-retrieval.

Resultaten

De evaluatie vond plaats op de FVEval Design2SVA benchmark met de Qwen3.5-35B en Mistral-Small-24B modellen.

Correctheid: ProofLoop bereikte een syntactische correctheid van 93,7% en een functionele correctheid van 82,0% met Qwen3.5. Dit is een enorme verbetering ten opzichte van de baseline (direct prompting), die slechts 43,2% functionele correctheid haalde.
Complexiteit: De voordelen van ProofLoop worden groter naarmate het ontwerp complexer wordt. Waar de baseline prestaties verliest bij multi-module ontwerpen (vanwege context-limieten), blijft ProofLoop stabiel door de modulaire RAG-aanpak.
Ablatie-studie: De studie bevestigde dat alle componenten (RAG, structurele analyse en de verificatie-loop) essentieel zijn. De grootste winst kwam voort uit de structurele analyse en de iteratieve verificatie-loop.

Betekenis en Conclusie

Dit onderzoek bewijst dat de integratie van LLM's met traditionele EDA-tools (Electronic Design Automation) de beperkingen van puur taalgebaseerde modellen kan overwinnen. Door de agent toegang te geven tot de "fysieke" waarheid van het hardwareontwerp via formele tools, wordt de vertaling van natuurlijke taal naar strikte logische specificaties betrouwbaar genoeg voor industriële toepassingen. Dit legt de basis voor een nieuwe generatie autonome verificatie-agenten die de productiviteit van hardware engineers aanzienlijk kunnen verhogen.