🤖 AI

NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

Dit artikel presenteert NeuroAbs, een neuro-symbolisch framework dat LLM's gebruikt voor RTL-signaalidentificatie en AST-gebaseerde symbolische representatie, gecombineerd met SMT-gebaseerde soundness-controle en CEGAR-verfijning, om RTL-abstractie te automatiseren en hardware-eigenschapscontrole aanzienlijk te versnellen.

Oorspronkelijke auteurs: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

Gepubliceerd 2026-08-19

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

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

In de verborgen wereld van moderne elektronica worden de chips die onze telefoons, auto's en computers aandrijven, gebouwd uit miljarden minuscule schakelaars. Voordat deze chips ooit worden geproduceerd, moeten ingenieurs bewijzen dat ze zich precies zullen gedragen zoals bedoeld, ongeacht welke instructies ze ontvangen. Dit proces, bekend als formele verificatie, is een rigoureuze wiskundige controle die ervoor zorgt dat een ontwerp vrij is van verborgen gebreken. Echter, naarmate deze ontwerpen complexer worden, wordt de taak om ze te controleren overweldigend. Het enorme aantal mogelijke toestanden waarin een chip terecht kan komen, is zo groot dat zelfs de krachtigste computers moeite hebben om ze allemaal binnen een redelijke tijd te verkennen. Om dit op te lossen, gebruiken ingenieurs vaak een techniek genaamd abstractie, wat een complex ontwerp vereenvoudigt door details te verwijderen die er niet toe doen voor een specifieke test, vergelijkbaar met het kijken naar een kaart van een stad die alleen de hoofdwegen toont die nodig zijn voor een specifieke reis, terwijl zijstraten en steegjes worden genegeerd.

Jarenlang vereiste het maken van deze vereenvoudigde modellen ofwel tijdrovend handmatig werk door menselijke experts, of het leunde op starre, vooraf geprogrammeerde regels die vaak de nuances van een specifiek ontwerp misten. Een nieuwe aanpak genaamd NeuroAbs biedt een ander pad, waarbij de kracht van patroonherkenning van kunstmatige intelligentie wordt gecombineerd met de strikte logica van de formele wiskunde. Deze methode gebruikt large language models—geavanceerde AI-systemen die getraind zijn op enorme hoeveelheden tekst—om de intentie achter een hardwareontwerp en een specifieke eigenschap die het moet voldoen, te begrijpen. De AI identificeert welke onderdelen van het circuit irrelevant zijn voor de huidige test en stelt voor hoe deze te vereenvoudigen. Omdat AI echter soms fouten kan maken of wijzigingen kan voorstellen die de logica breken, vertrouwt het systeem de AI niet blindelings. In plaats daarvan fungeert het als een neuro-symbolisch framework, waarbij de AI wijzigingen voorstelt en een aparte, rigoureuze wiskundige engine onmiddellijk controleert of die wijzigingen veilig zijn. Als de vereenvoudiging te agressief is en het risico loopt een echte fout te verbergen, verfijnt het systeem het model automatisch, waarbij de lagen van vereenvoudiging net genoeg wordt teruggepeld om de nauwkeurigheid te herstellen zonder de snelheidvoordelen te verliezen.

De onderzoekers achter NeuroAbs testten hun framework op verschillende real-world processorontwerpen en perifere componenten, waaronder een veelgebruikte communicatie-interface die in veel apparaten wordt gebruikt. Ze ontdekten dat het systeem erin slaagde om kansen te identificeren om de logica te vereenvoudigen die traditionele regelgebaseerde methoden misten. Wanneer bijvoorbeeld een specifieke instructie in een processor werd geverifieerd, realiseerde de AI zich dat de logica die andere, ongerelateerde instructies afhandelt, veilig kon worden vervangen door een generieke placeholder. Dit stelde de verificatie-engine in staat om zich alleen op de relevante delen van het circuit te concentreren. In experimenten versnelde deze aanpak de tijd die nodig is om te bewijzen dat een ontwerp correct is aanzienlijk. Wanneer de onderzoekers NeuroAbs integreerden met bestaande hoogwaardige verificatietools, daalde de tijd die nodig was om een formeel bewijs te bereiken in veel gevallen met bijna de helft. Zelfs wanneer een volledig bewijs niet mogelijk was binnen de tijdslimiet, stelden de vereenvoudigde modellen het systeem in staat om veel dieper in het gedrag van het circuit te verkennen, waardoor potentiële bugs aan het licht kwamen die anders verborgen zouden zijn gebleven.

Het succes van deze methode berust op een zorgvuldige balans tussen de flexibiliteit van de AI en de precisie van de formele logica. Het systeem analyseert eerst het ontwerp en het specifieke testszenario om aan te wijzen welke signalen cruciaal zijn. Vervolgens gebruikt het de AI om de code in die specifieke gebieden te herschrijven, waarbij complexe berekeningen worden vervangen door simpelere, abstracte waarden. Cruciaal is dat elke herschrijving wordt onderworpen aan een strikte wiskundige controle om te garanderen dat het de fundamentele werking van de chip niet op een manier verandert die de test ongeldig maakt. Als de controle faalt, gebruikt het systeem een feedbackloop om exact te identificeren welke vereenvoudiging het probleem veroorzaakte en keert het dat specifieke deel terug naar de oorspronkelijke vorm. Dit iteratieve proces zorgt ervoor dat het uiteindelijke model zowel eenvoudig genoeg is om snel te verifiëren als nauwkeurig genoeg om vertrouwd te worden. De resultaten laten zien dat deze hybride aanpak diverse soorten hardwarelogica kan afhandelen, van eenvoudige rekenkundige operaties tot complexe vertakkende structuren, wat het een krachtig hulpmiddel maakt voor de volgende generatie chipontwerp.

Door de creatie van deze vereenvoudigde modellen te automatiseren, pakt NeuroAbs een belangrijke flessenhals in de hardware engineering aan. Voorheen hing de beslissing over wat te vereenvoudigen en hoe dat te doen af van menselijke intuïtie of vaste regels die niet konden worden aangepast aan elke unieke ontwerpuitdaging. Dit nieuwe framework laat zien dat kunstmatige intelligentie effectief kan worden aangestuurd om deze taken uit te voeren, mits deze wordt verankerd door een systeem dat elke stap verifieert. De bevindingen suggereren dat de toekomst van hardwareverificatie kan liggen in dergelijke collaboratieve systemen, waarbij machines het zware werk van patroonherkenning en suggestie afhandelen, terwijl wiskundige strengheid de veiligheid en juistheid van het eindproduct waarborgt. Naarmate chipontwerpen in complexiteit blijven groeien, bieden tools zoals NeuroAbs een veelbelovende manier om het tempo bij te houden, zodat de apparaten waarop we vertrouwen gebouwd worden op een fundament van geverifieerde waarheid.

Technische Samenvatting: NeuroAbs

Probleemstelling

Formele verificatie, specifiek property checking (model checking), is essentieel voor het waarborgen van de functionele correctheid van hardware-ontwerpen. Echter, naarmate Register-Transfer-Level (RTL) ontwerpen in omvang en complexiteit groeien, wordt het efficiënt bewijzen van door de gebruiker gespecificeerde eigenschappen (properties) een significante bottleneck. Hoewel abstractietechnieken veelal worden gebruikt om de systeemcomplexiteit te verminderen door concrete modellen te vervangen door vereenvoudigde representaties, kampen bestaande methoden met twee primaire beperkingen:

Handmatige Abstractie: Leunt zwaar op menselijk inzicht en is arbeidsintensief, omdat ingenieurs handmatig moeten identificeren welke delen van het ontwerp irrelevant zijn voor een specifieke eigenschap.
Regelgebaseerde Automatische Abstractie: Technieken zoals structurele abstractie, syntax-gestuurde abstractie en datapath-abstractie (bijv. het vervangen van rekenkundige operaties door ongeïnterpreteerde functies) missen flexibiliteit. Ze slagen er vaak niet in om abstractiekansen te identificeren die afhangen van de specifieke semantische intentie van een verificatiescenario en de doel-eigenschap, omdat ze vertrouwen op vooraf gedefinieerde syntactische regels in plaats van functioneel begrip.

Gevolgelijk missen huidige methoden vaak kansen om logica die irrelevant is voor een specifieke verificatiedoelstelling veilig te abstraheren, of produceren ze abstracties die ofwel te grof zijn (wat leidt tot spookige tegenvoorbeelden/spurious counterexamples) of te conservatief (waardoor de verificatie niet versnelt).

Methodologie: Het NeuroAbs-framework

Het paper stelt NeuroAbs voor, een neuro-symbolisch framework dat Large Language Models (LLMs) integreert met symbolische redenering om RTL-abstractie te automatiseren. Het framework werkt in drie afzonderlijke fasen:

1. LLM-ondersteunde Signaalanalyse (Neuraal Component)

In plaats van volledige RTL-codebases naar een LLM te voeden, wat de contextlimieten overschrijdt, gebruikt NeuroAbs een Signal Analyzer om kandidaat-signalen voor abstractie te identificeren.

Input: Ontwerpspecificaties, beschrijvingen van verificatiescenario's en signaaldefinities.
Proces: Met behulp van Chain-of-Thought (CoT) prompting en aangepaste systeeminstructies analyseert de LLM het verificatiescenario om "scenario-gerelateerde signalen" te identificeren. Het bepaalt welke signalen de logica controleren die relevant is voor de specifieke eigenschap en stelt vaste waarden voor (bijv. het instellen van een opcode op een specifiek instructietype).
Integratie van Statische Analyse: De output van de LLM wordt gecombineerd met RTL-statische analyse (bijv. constante propagatie) om de specifieke codegebieden en statements te lokaliseren die door deze signalen worden beïnvloed. Dit verkleint de scope van het gehele ontwerp naar een kleine set kandidaat-statements.

2. AST-gestuurde Abstractie (Neuro-Symbolische Kern)

Om de structurele integriteit te waarborgen en te voorkomen dat de LLM niet-gerelateerde logica herschrijft, zet NeuroAbs de RTL om in een Abstract Syntax Tree (AST).

Lokalisatie: Het systeem brengt de geïdentificeerde kandidaat-signalen in kaart naar specifieke statement-niveau AST-nodes en hun omringende structurele contexten (bijv. always blocks, case statements).
Transformatie: Een tweede LLM, de Abstractor, krijgt de taak om alleen de gelokaliseerde AST-nodes te herschrijven. Het maakt gebruik van few-shot learning (het verstrekken van voorbeelden van originele versus geabstraheerde statements) om kandidaat-abstracties te genereren.
Restrictie: De LLM is beperkt tot het herschrijven van enkel de specifieke delen van een statement die als irrelevant voor de eigenschap worden beschouwd (bijv. het vervangen van een AND-operatie met een onbekende waarde X als de eigenschap alleen betrekking heeft op ADD-operaties), terwijl de relevante logica behouden blijft.

3. Symbolische Validatie en Verfijning (Symbolisch Component)

Elke gegenereerde abstractie wordt rigoureus gevalideerd om te garanderen dat het een geldige over-approximatie is van het originele ontwerp.

SMT Checking: Het framework gebruikt Satisfiability Modulo Theories (SMT) solvers (specifiek Z3) om de conditie $\forall V, S(V) \implies \hat{S}(V)$ $\forall V, S (V) ⟹ \hat{S} (V)$ te verifiëren. Dit zorgt ervoor dat elke gedraging die toegestaan is door het geabstraheerde statement ook toegestaan is door het originele statement.
- Afhandeling van X-waarden: Omdat SMT-solvers niet van nature ondersteuning bieden voor onbekende waarden (X), worden deze vertaald naar verse variabelen die gebonden zijn aan existentiële kwantoren ( $\exists Y$ ), zodat de solver ze kan behandelen als niet-deterministische keuzes.
Gecustomiseerde CEGAR-loop (R-CEGAR): Als het abstracte model de eigenschap niet kan bewijzen en een tegenvoorbeeld genereert, controleert het systeem of het tegenvoorbeeld spookig (spurious) is.
- Indien het spookig is, wordt een counterexample reduction techniek toegepast om het spoor te generaliseren en exact te pinpointen welk geabstraheerd statement de schending heeft veroorzaakt.
- Het systeem keert vervolgens alleen de specifieke ongeldige statements terug naar hun originele vorm, in plaats van de gehele abstractie te verwerpen, en iterat de procedure.

Belangrijkste Bijdragen

Eerste toepassing van LLMs op RTL-abstractie: Het paper introduceert NeuroAbs als het eerste framework dat LLMs gebruikt voor het identificeren en genereren van RTL-abstracties, waarmee het verder gaat dan statische regelgebaseerde benaderingen.
Neuro-symbolische workflow: Het stelt een nieuw proces voor waarbij het neurale component (LLM) scenario-bewuste kandidaten voorstelt, terwijl het symbolische component (AST-traversal en SMT) de herschrijving beperkt tot precieze structurele doelwitten en de geldigheid valideert.
Gecustomiseerde verfijning (R-CEGAR): De auteurs introduceren een verfijningsloop die counterexample reduction gebruikt om efficiënt te identificeren en alleen de specifieke abstracte statements terug te draaien die voor spookige tegenvoorbeelden zorgen, waardoor het aantal benodigde iteraties wordt geminimaliseerd.

Experimentele Resultaten

Het framework werd geëvalueerd op een reeks benchmarks, waaronder RISC-V processorcores (PicoRV32, Piccolo, Flute) en een I2C-perifeer, die 55 verificatiescenario's beslaan. De resultaten werden vergeleken met state-of-the-art model checkers (AVR en RIC3) die reeds geavanceerde abstractiemechanismen bevatten.

Versnelling van Formele Bewijsvoering: Wanneer geïntegreerd met AVR, reduceerde NeuroAbs de gemiddelde runtime voor het construeren van formele bewijzen met 44,89%. Zelfs met de bestaande abstractiecapaciteiten van AVR, leverde NeuroAbs significante extra versnellingen.
Efficiëntie bij Bug-vinden (BMC): In gevallen waarin formele bewijzen niet binnen de tijdslimiet konden worden voltooid, versnelde NeuroAbs het Bounded Model Checking (BMC) proces aanzienlijk.
- In het "Piccolo"-geval nam de gemiddelde unrolling depth toe van 109,36 naar 125,36 cycli.
- In het "Flute"-geval werd de tijd die nodig is om de maximale diepte van de baseline te bereiken met 75,98% verminderd.
Ablatie-studies: Experimenten bevestigden dat zowel few-shot learning als custom instructies cruciaal zijn. Het verwijderen van few-shot learning liet de over-approximatie ratio dalen van 95,27% naar 83,51%. Het verwijderen van custom instructies leidde tot een daling van 98,38% in "strikte" over-approximaties (wat betekent dat het model de neiging had om originele statements te reproduceren in plaats van ze te abstraheren).
Complexiteitsreductie: Analyse van de resulterende And-Inverter-Gate (AIG) circuits toonde een substantiële reductie in de maximale variabele index, wat bevestigt dat NeuroAbs de circuitstructuur effectief vereenvoudigt.

Betekenis en Claims

Het paper claimt dat NeuroAbs de starheid van traditionele regelgebaseerde abstractie en de arbeidsintensiviteit van handmatige methoden aanpakt. Door de semantische redeneerkracht van LLM's te combineren met de strikte discipline van symbolische verificatie, kan NeuroAbs scenario-specifieke abstractiekansen identificeren die statische regels missen.

De auteurs positioneren NeuroAbs niet als een vervanging voor bestaande model checkers, maar als een complementair framework dat hun efficiëntie verhoogt. De resultaten laten zien dat zelfs wanneer het wordt geïntegreerd met hoog geoptimaliseerde, winnende model checkers (AVR en RIC3), de neuro-symbolische aanpak meetbare verbeteringen oplevert in zowel de snelheid van bewijsconstructie als de diepte van het vinden van bugs. Het framework wordt gepresenteerd als een stap richting meer geautomatiseerde, scenario-bewuste hardwareverificatie die de afhankelijkheid van handmatige expertise vermindert.