Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

In de onzichtbare wereld van microchips, waar miljarden transistors aan- en uitschakelen om alles van smartphones tot ruimtevaartuigen van stroom te voorzien, kan één enkele verborgen fout een systeem catastrofaal laten falen. Ingenieurs ontwerpen deze chips met behulp van een taal die Register Transfer Level wordt genoemd, of RTL, die beschrijft hoe gegevens in de loop van de tijd tussen opslagelementen bewegen. Om ervoor te zorgen dat deze ontwerpen correct werken voordat ze worden gebouwd, schrijven verificatie-experts "assertions" (beweringen). Beschouw een assertion als een strikte regel die in het ontwerp zelf is geschreven, een stelling die zegt: "Als dit gebeurt, dan moet dat volgen." Als de chip deze regel ooit schendt, slaat het systeem alarm, waardoor een bug aan het licht komt die anders onopgemerkt zou blijven. Decennialang was het schrijven van deze regels een langzame, handmatige en foutgevoelige taak, waarbij ingenieurs moesten raden welke gedragingen fout zouden kunnen gaan en specifieke controles voor hen moesten schrijven. Hoewel computers hebben geholpen door bestaande design-simulaties te minen om patronen te vinden, missen deze geautomatiseerde methoden vaak de meest gevaarlijke scenario's, simpelweg omdat de willekeurige tests waarop ze vertrouwen nooit op die scenario's stuiten.

Een team onderzoekers van The Hong Kong University of Science and Technology (Guangzhou) heeft een nieuwe aanpak ontwikkeld om dit probleem op te lossen, genaamd NeuroAssertion. In plaats van te vertrouwen op toeval om bugs te vinden, zoekt hun methode actief naar de moeilijkst te bereiken gedragingen in een chipontwerp en gebruikt vervolgens een combinatie van kunstmatige intelligentie en formele logica om de noodzakelijke veiligheidsregels te schrijven. Het proces begint met het transformeren van het ontwerp om het gemakkelijker te maken om te zien welke onderdelen worden getest. De onderzoekers voegen speciale markers toe aan de code die bijhouden of specifieke, moeilijk te triggeren condities ooit zijn opgetreden. Vervolgens gebruiken ze een krachtige wiskundige engine, een model checker genoemd, om het ontwerp te dwingen die zeldzame condities uit te voeren. Dit genereert een reeks zeer specifieke testgevallen die gedragingen blootleggen die willekeurige simulaties waarschijnlijk voor altijd zouden missen. Deze nieuwe, diverse traces bieden een veel rijker fundament voor de volgende stap.

Zodra het systeem deze moeilijk te vinden gedragingen heeft, gaat het over naar de generatiefase. Het maakt gebruik van een techniek genaamd syntax-guided synthesis om initiële veiligheidsregels te creëren op basis van de geobserveerde gegevens. De onderzoekers erkenden echter dat deze eerste passage zelden perfect is. Om dit op te lossen, introduceerden ze een verfijningslus die fungeert als een rigoureuze redacteur. Het systeem meet hoe goed de huidige set regels veranderingen in het ontwerp kan detecteren door kleine, bewuste fouten, bekend als mutanten, in de code te injecteren. Als de regels een mutant niet kunnen detecteren, weet het systeem precies welk gedrag onontdekt is gebleven. Het roept vervolgens een groot taalmodel aan om een nieuwe regel voor te stellen die specifiek is ontworpen om dat gat te dichten. Als de voorgestelde regel logisch gebrekkig is, gooit een tweede taalmodel deze niet weg; in plaats daarvan analyseert het de fout en construeert het een gespecialiseerde set instructies, of een grammatica, om een symbolische solver te begeleiden bij het repareren van de regel. Dit creëert een cyclus waarin het systeem claims voorstelt, controleert en corrigeert totdat ze zowel talrijk als robuust zijn.

De resultaten van deze aanpak werden getest op zeven verschillende chipontwerpen, variërend van kleine arbitragecircuits tot complexe processorcores. Het nieuwe framework presteerde consequent beter dan de huidige state-of-the-art methode, bekend als SMART, die vertrouwt op een enkele pass van mining zonder deze actieve verfijning. In deze experimenten genereerde NeuroAssertion ongeveer twee keer zoveel assertions als de oudere methode. Belangrijker nog was dat de kwaliteit van deze regels aanzienlijk hoger was. Wanneer gemeten aan hun vermogen om geïnjecteerde fouten te detecteren, bereikte het nieuwe systeem ongeveer twee keer de dekking van de traditionele aanpak. Op sommige specifieke benchmarks was de verbetering zelfs nog spectaculairder; bijvoorbeeld, op één component van een processor sprong de mutatie-dekking van ongeveer zes procent naar meer dan tweeëndertig procent. De onderzoekers vergeleken hun systeem ook met een directe aanpak waarbij een groot taalmodel werd gevrand om regels te schrijven zonder enige formele controle of verfijningsstappen. Die directe methode produceerde veel minder regels en slaagde er niet in om de meeste potentiële fouten te detecteren, wat aantoont dat pure taalgeneratie alleen onvoldoende is voor deze cruciale taak.

Door het genereren van assertions te behandelen als een continue lus van exploratie en verfijning in plaats van een eenmalige gebeurtenis, hebben de onderzoekers aangetoond dat het mogelijk is om de creatie van hoogwaardige veiligheidsregels voor complexe hardware te automatiseren. Het systeem raadt niet alleen; het zoekt actief naar de blinde vlekken in een ontwerp en gebruikt een partnerschap tussen neurale netwerken en formele logica om deze in te vullen. Dit werk suggereert dat de toekomst van hardwareverificatie ligt in het combineren van de patroonherkenning van kunstmatige intelligentie met de rigoureuze zekerheid van wiskundige bewijsvoering, om ervoor te zorgen dat de chips die onze wereld aandrijven even betrouwbaar zijn als de ingenieurs die ze ontwerpen.