FormalRTL: Verified RTL Synthesis at Scale

Dit paper introduceert FormalRTL, een nieuw multi-agent raamwerk dat software-referentiemodellen gebruikt als formele specificaties om betrouwbare en schaalbare RTL-codegeneratie voor complexe industriële ontwerpen mogelijk te maken.

De kern

Stel je voor dat je een enorm, complex machine moet bouwen, zoals een nieuwe chip voor een supercomputer. In het verleden deden ingenieurs dit handmatig: ze schreven duizenden regels code, regel voor regel, en hoopten dat het werkte. Als er een foutje in zat, duurde het dagen om het te vinden.

Nu proberen we kunstmatige intelligentie (AI) om dit werk te laten doen. Maar tot nu toe was de AI als een zeer creatieve, maar soms verwarde leerling. Als je hem vroeg: "Bouw een rekenmachine," maakte hij misschien een mooie machine, maar de knoppen werkten niet altijd zoals bedoeld, of hij vergat de batterij. De AI was goed in het schrijven van code, maar slecht in het garanderen dat die code foutloos was.

FormalRTL is een nieuwe, slimme manier om AI te gebruiken voor het bouwen van deze chips. Het is als het geven van een onfeilbare bouwplaat en een strenge inspecteur aan die AI-leerling.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. Het Probleem: De "Vage Instructie"

Stel je voor dat je een kok (de AI) vraagt om een complexe taart te bakken, maar je geeft alleen een beschrijving: "Het moet lekker zijn en rond." De kok probeert het, maar de taart valt in elkaar.
In de chipwereld is dit wat er gebeurt als je AI alleen een tekstuele beschrijving geeft. De AI raakt in de war over de details (zoals hoe getallen worden opgeslagen of hoe snel de klok moet tikken).

2. De Oplossing: De "Gouden Recept" (Software Referentiemodel)

Bij FormalRTL geven we de kok niet alleen een tekst, maar ook een perfect, getest recept (een computerprogramma in C/C++). Dit recept is de "gouden standaard".

• De AI weet precies wat hij moet doen: Hij kijkt naar het recept en zegt: "Oké, ik moet dit ingrediënt (deel van de chip) precies zo maken als in het recept."
• Geen giswerk meer: Omdat het recept al klopt, hoeft de AI niet te raden hoe de logica werkt.

3. Het Bouwproces: De "Meester-Bouwploeg"

FormalRTL gebruikt geen enkele AI, maar een team van drie gespecialiseerde agenten (AI-assistenten) die samenwerken:

• De Plannings-Agent (De Architect):
  In plaats van de hele taart in één keer te proberen te bakken, kijkt deze agent naar het recept en zegt: "Laten we eerst de bodem maken, dan de vulling, en pas daarna de glazuur." Hij breekt het enorme project op in kleine, beheersbare stukjes. Dit voorkomt dat de AI overweldigd raakt door de complexiteit.

• De Bouw-Agent (De Bakker):
  Deze agent bouwt elk klein stukje (bijvoorbeeld een vermenigvuldiger) op basis van het recept. Hij schrijft de code voor de chip.

• De Controleur & Reparateur (De Kwaliteitsinspecteur):
  Dit is het belangrijkste deel. Zodra de AI een stukje code heeft geschreven, wordt het direct getest tegen het "gouden recept".

  • Stel: De AI bouwt een brug, maar de brug is 1 meter te kort.
  • De inspecteur zegt niet alleen: "Fout!" (zoals een simpele test). Hij geeft een specifiek bewijs: "De brug is te kort omdat je de steunpilaar op de verkeerde coördinaat hebt gezet."
  • De AI krijgt dit bewijs, begrijpt de fout, en repareert het direct. Dit proces herhaalt zich tot de brug perfect past.

4. Waarom is dit zo belangrijk?

Vroeger moesten ingenieurs duizenden testcases schrijven om te zien of een chip werkte. Dat was als proberen te raden of een auto veilig is door er met verschillende snelheden tegenaan te rijden.
Met FormalRTL is het alsof je een wiskundig bewijs hebt: "Deze chip werkt 100% hetzelfde als het perfecte recept."

• Schaalbaarheid: Het werkt zelfs voor enorme projecten (meer dan 1000 regels code), wat voorheen onmogelijk was voor AI.
• Betrouwbaarheid: Het systeem garandeert dat de chip geen verborgen fouten heeft, zelfs niet in de rare, zeldzame situaties (de "hoekgevallen") waar andere methoden vaak falen.

Samenvattend

FormalRTL is als het geven van een onfeilbare bouwtekening en een slimme, strenge inspecteur aan een AI. In plaats van dat de AI probeert te gokken hoe een chip moet werken, volgt hij een bewezen plan en wordt elke stap direct gecontroleerd. Hierdoor kunnen we nu sneller, veiliger en betrouwbaarder de chips van de toekomst bouwen, van AI-chips tot de processoren in onze telefoons.

De auteurs van het paper hebben dit systeem openbaar gemaakt, zodat andere onderzoekers en bedrijven het ook kunnen gebruiken om de toekomst van hardware te versnellen.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "FormalRTL: Verified RTL Synthesis at Scale" in het Nederlands.

Probleemstelling

Hoewel Large Language Models (LLM's) veelbelovend zijn gebleken voor het automatiseren van hardware-synthese, blijven er aanzienlijke barrières bestaan voor industriële toepassingen, met name voor datapath-gerichte ontwerpen. De huidige methoden kampen met twee fundamentele uitdagingen:

1. Complexiteit van grootschalig ontwerp: Industriële IP-kernen vereisen duizenden regels RTL-code. Bestaande planning-methoden, die vaak alleen vertrouwen op ongestructureerde natuurlijke taal-specificaties, hebben moeite met het nemen van sounde architecturale beslissingen en het omgaan met ambiguïteiten.
2. Ingewikkelde rekenkundige en logische structuren: Industriële ontwerpen bevatten diep geneste datapaths en aangepaste datatypes (zoals bfloat16 of hifloat8). Simulatie-gebaseerde verificatie faalt vaak bij het dekken van randgevallen (corner cases), wat essentieel is voor datapath-rijke ontwerpen.

De kern van het probleem is dat het direct synthetiseren van RTL-code vanuit natuurlijke taal-specificaties onvoldoende is om de complexe structurele, temporale en rekenkundige eisen van hardware te garanderen. In de industrie vertrouwen ingenieurs traditioneel op software-referentiemodellen (vaak in C/C++) als "gouden specificaties" voor formele verificatie, maar deze bron wordt door bestaande LLM-gedreven synthesemethoden grotendeels genegeerd.

Methodologie: FormalRTL

FormalRTL is een nieuw end-to-end multi-agent framework dat software-referentiemodellen gebruikt als formele, uitvoerbare specificaties om de generatie en verificatie van Register-Transfer Level (RTL) code te sturen. Het systeem integreert planning, synthese en formele equivalentiecontrole (EC) in een gesloten lus.

Het workflow bestaat uit drie hoofdagenten:

1. Planning Agent:

   • Voert statische analyse uit op het C-referentiemodel (via een compiler zoals Clang) om de abstract syntax tree (AST) te analyseren.
   • Deelt het complexe ontwerp op in modulaire subtaken gebaseerd op functie-afhankelijkheden in de C-code.
   • Refactoriseert de algemene specificatie naar gerichte specificaties voor elke submodule.
   • Genereert de code in een strikte topologische volgorde van de afhankelijkheden, wat zorgt voor een betrouwbare planning die minder afhankelijk is van vage natuurlijke taal.

2. Initializing Agent:

   • Genereert voor elke submodule de initiële RTL-code en een bijbehorende verificatie-harness.
   • De harness stelt een verificatieomgeving in waarbij de invoer voor zowel de C-code als de RTL-code identiek wordt verondersteld en de output-equivalentie wordt geasserteerd.
   • Bepaalt de noodzakelijke tijdsraam (clock cycles) voor sequentiële logica, wat essentieel is voor transactie-equivalentiecontrole.

3. Debugging Agent:

   • Gebruikt feedback van een formele equivalentiecontrole-tool (hw-cbmc) om fouten op te lossen.
   • Bug Locator: Identificeert de positie van syntaxisfouten en presenteert de omliggende code aan de LLM.
   • CE Simplifier (Counterexample): Vereenvoudigt tegenvoorbeelden uit de EC-tool om alleen de relevante functies en mismatchende signalen te tonen.
   • De LLM gebruikt deze gefocuste feedback om patches te genereren en de code te corrigeren, waardoor een geautomatiseerde iteratieve cyclus ontstaat totdat formele equivalentie is bereikt.

Belangrijkste Bijdragen

• Software-Referentiemodel-gedreven Methodologie: Een pionierende aanpak die C/C++ modellen gebruikt als formele specificaties voor agile hardware-ontwikkeling, in plaats van te vertrouwen op alleen natuurlijke taal.
• End-to-End Multi-Agent Engine: Een geautomatiseerd systeem dat planning, synthese, debugging en formele verificatie integreert, waarbij statische analyse en equivalentiecontrole de kern vormen.
• Industriële Benchmark Suite: Het creëren en openen van een nieuwe set benchmarks met complexe, datapath-rijke modules (zoals FP16 en Hifloat8 operatoren) inclusief specificaties en software-referentiemodellen, wat ontbreekt in bestaande open-source datasets.

Resultaten

De auteurs hebben FormalRTL getest op een reeks academische en industriële benchmarks (tot meer dan 1000 regels code).

• Succespercentages: Hoewel de Initial Success Rate (ISR) voor complexe modules laag is (wat aantoont dat LLM's het moeilijk hebben met de eerste poging), bereikt het systeem een hoge Final Success Rate (FSR) dankzij de effectieve debugging-agent. Bijvoorbeeld, voor de "hifloat8_mul" module werd een FSR van 100% bereikt.
• Efficiëntie van Debugging: De gebruikte tegenvoorbeeld-geleide debugging (Counterexample-Guided Debugging) is aanzienlijk efficiënter dan binaire "pass/fail" feedback. Zonder deze tools daalde de FSR drastisch (van 95% naar 55% in ablatiestudies).
• Schalbaarheid: In vergelijking met een baseline die alleen op specificaties baseert (zonder C-referentiemodel), presteert FormalRTL veel beter bij toenemende complexiteit. Waar de baseline faalde bij complexe ontwerpen (0% succes), behield FormalRTL een hoge stabiliteit.
• Kwaliteit van het Resultaat (QoR): De gegenereerde RTL-code heeft iets minder optimale oppervlakte en vertraging dan handmatig ontworpen code (door de focus op correctheid boven PPA-optimalisatie), maar biedt een correct, uitvoerbaar fundament dat ingenieurs kan gebruiken voor verdere optimalisatie.

Betekenis en Toekomstperspectief

FormalRTL sluit de kloof tussen academische prototypes en industriële hardware-ontwikkeling door formele correctheidsgaranties te bieden in een schaalbaar proces. De belangrijkste implicaties zijn:

• Het bewijst dat het gebruik van software-referentiemodellen cruciaal is voor het overwinnen van de ambiguïteit in natuurlijke taal-specificaties.
• Het biedt een robuust kader voor het genereren van complexe datapath-ontwerpen die anders moeilijk te verifiëren zijn.
• Het benadrukt de noodzaak van betere open-source tools voor C-RTL equivalentiecontrole en de ontwikkeling van gespecialiseerde LLM's voor het interpreteren van debugging-feedback.

Dit werk markeert een belangrijke stap naar betrouwbare, geautomatiseerde hardware-synthese voor de toekomstige generatie AI-chips en andere rekenintensieve systemen.