Technische Samenvatting: SpecAlign – Een Semantisch Uitlijningskader voor SystemVerilog Assertiegeneratie

1. Probleemstelling

De toenemende complexiteit van moderne hardwareontwerpen heeft de adoptie van Large Language Models (LLM's) voor het genereren van SystemVerilog Asserties (SVA) ter ondersteuning van Assertion-Based Verification (ABV) gestimuleerd. Echter, bestaande LLM-benaderingen richten zich voornamelijk op syntactische validiteit en resultaten van formele verificatie (FV) (bijvoorbeeld of een assertie bewezen is of een tegenvoorbeeld oplevert op een gegeven RTL). Deze metrieken slagen er niet in om semantische uitlijning aan te pakken: of de gegenereerde assertie de gedragsintentie die in de natuurlijke taalspecificatie wordt beschreven, nauwkeurig weerspiegelt.

LLM's kunnen asserties produceren die syntactisch correct en formeel bewijsbaar zijn op een specifieke RTL-implementatie, maar semantisch inefficiënt of hallucinerend zijn. Bijvoorbeeld, een assertie kan een klok bemonsteren op dezelfde flank die de eigenschap triggert, waardoor deze vacuüm wordt ondanks het doorstaan van FV. Bij afwezigheid van een "golden" RTL-model voor vergelijking is handmatige inspectie van dergelijke asserties tijdrovend en verlaagt het het vertrouwen. Bovendien kampen FV-motoren met schaalbaarheidsproblemen (explosie van de toestandsruimte) bij het evalueren van grote sets gegenereerde asserties voor complexe ontwerpen. Er is een kritieke behoefte aan een kader dat semantische consistentie tegenover de specificatie zelf evalueert, onafhankelijk van RTL-implementatiedetails.

2. Methodologie: Het SpecAlign-kader

SpecAlign is een specificatiegericht kader dat is ontworpen om door LLM's gegenereerde SVAs te evalueren en iteratief te verfijnen zonder afhankelijk te zijn van een golden RTL. Het werkt via twee primaire iteratieve lussen: een Eigenschap-uitlijningslus en een SVA-uitlijningslus. Beide lussen maken gebruik van drie kernfasen: Uitlijningscontrole, Inconsistentie-analyse en Evidentie-extractie.

A. Architecturale Overzicht

Het kader normaliseert de vergelijking tussen verschillende representaties van ontwerintentie. Hoewel de invoer bestaat uit natuurlijke taaleigenschappen ($P$) en gegenereerde SVAs ($A$), converteert het kader elke SVA naar een Natuurlijke Taal Samenvatting ($N$) via een specifiek extractieproces. Deze normalisatie stelt zowel eigenschappen als asserties in staat om op hetzelfde semantische niveau te worden geëvalueerd tegenover de ontwerpspecificatie ($S$).

B. Kerncomponenten

1. Uitlijningscontrole:

   • Classificatie: Het kader classificeert beschrijvingen in natuurlijke taal ($X_i$) in drie categorieën op basis van hun relatie met de specificatie:
     • Impliceert (Entails): Alle elementen worden ondersteund door de specificatie.
     • Weerspreekt (Contradicts): Minstens één element weerspreekt de specificatie.
     • Onbekend: Elementen worden noch ondersteund noch weerlegd (vaak vanwege implementatiespecifieke aannames die niet in de specificatie staan).
   • Zelfconsistentie-stemming: Om de betrouwbaarheid te verbeteren, hanteert het systeem een Chain-of-Thought (CoT) prompting-strategie. Het genereert $k$ redeneerpaden voor een gegeven invoer en aggregeert de sub-verdicts met meerderheidsstemming. Bij een gelijkspel wordt een conservatieve prioriteit toegepast: Weerspreekt > Onbekend > Impliceert.
   • Referentiekeuze: De Eigenschapslus gebruikt de ontwerpspecificatie ($S$) als referentie. De SVA-lus gebruikt een "Gelijkgerichte Eigenschapsbank" (indien beschikbaar) om ruis van verspreide specificatiedocumenten te verminderen; anders valt het terug op $S$.

2. Inconsistentie-analyse & Verfijning:

   • Wanneer een verdict Weerspreekt is, voert het systeem een Inconsistentie-analyse uit. Het identificeert de specifieke conflicterende elementen in de beschrijving, verwijst naar het juiste gedrag in de specificatie en genereert gestructureerde, actieerbare feedback ($F_i$).
   • Deze feedback leidt de LLM om de eigenschap of assertie ($P'_i$ of $A'_i$) opnieuw te genereren, waarbij triggercondities expliciet worden gedefinieerd en het introduceren van nieuwe signalen of gedragingen die niet in de specificatie voorkomen, wordt vermeden.
   • De verfijnde output wordt opnieuw geëvalueerd in de uitlijningslus totdat een vast aantal iteraties is bereikt of de output is uitgelijnd.

3. Evidentie-extractie:

   • Voor Impliceert-gevallen extrahert het systeem ondersteunende bewijslast (citaten en locaties) uit de specificatie om menselijke review te faciliteren en het vertrouwen te versterken.
   • Voor Onbekend-gevallen categoriseert het systeem welke elementen ambigu of ongedefinieerd zijn, en onderscheidt het ware tegenstrijdigheden van ondergespecificeerd gedrag.

4. Kwantitatieve Metriek:

   • Het kader definieert een Uitlijningsscore ($a_t$) berekend als de verhouding van geïmpliceerde asserties ($E$) tot het totale aantal asserties ($n$) op een gegeven iteratie ($a_t = E/n$). Het doel van het verfijningsproces is het maximaliseren van deze score.

C. Extractie van Natuurlijke Taal Samenvatting

Een kritieke voorverwerkingsstap bestaat uit het converteren van formele SVAs naar gestructureerde samenvattingen in natuurlijke taal. De LLM wordt geprompt om specifieke SVA-componenten (Trigger, Antecedent, Implicatie-operator, Consequent en Disable If) te identificeren en deze te mappen naar equivalente zinnen in natuurlijke taal. Dit zorgt ervoor dat de semantische intentie van de formele code behouden blijft voor vergelijking.

3. Belangrijkste Bijdragen

Het artikel schetst de volgende bijdragen:

• Semantisch Evaluatiekader: Een nieuwe aanpak om door LLM's gegenereerde SVAs te beoordelen tegenover specificaties in natuurlijke taal zonder afhankelijk te zijn van formele verificatie toegepast op een golden RTL.
• Iteratief Verfijningsproces: Een gestructureerd kader bestaande uit Uitlijningscontrole, Inconsistentie-analyse en SVA-samenvattingsextractie, ontworpen voor integratie in bestaande door LLM's gebaseerde generatieworkflows.
• Kwantitatieve Uitlijningsmetriek: Een uitlijningsscore-metriek gebaseerd op classificatie van semantische implicatie om specificatieconsistentie te meten, wat een schaalbaar alternatief biedt voor traditionele FV-correctheidsevaluatie.
• Inconsistentie-analyse Mechanisme: Een methode om specifieke, actieerbare feedback te genereren voor tegenstrijdige eigenschappen en asserties, ter ondersteuning van zowel handmatige review als geautomatiseerde verfijning.
• Empirische Validatie: Experimentele resultaten die de reductie van tegenstrijdige asserties in APB- en UART-ontwerpen aantonen door semantische verfijning.

4. Experimentele Resultaten

De auteurs evalueerden SpecAlign op twee hardwareontwerpen: APB (APB naar I2C-interface) en UART (UART naar Bus-interface). Het kader werd vergeleken met AssertionForge, een basismethode die een kennisgrafiek gebruikt en RTL integreert in de generatie.

• APB-resultaten:
  • Basislijn (AssertionForge): Genereerde 442 SVAs met een uitlijningsscore van 0,02. Slechts 8 waren geïmpliceerd, terwijl 148 tegenstrijdig waren.
  • SpecAlign: Behield 442 SVAs maar verhoogde de uitlijningsscore naar 0,15. Cruciaal, het aantal tegenstrijdige asserties daalde naar 0, met 66 geïmpliceerde asserties. De overige 376 werden geclassificeerd als Onbekend.
• UART-resultaten:
  • Basislijn: Genereerde 325 SVAs met een uitlijningsscore van 0,06 (21 geïmpliceerd, 142 tegenstrijdig).
  • SpecAlign: Genereerde 319 SVAs met een uitlijningsscore van 0,28. Tegenstrijdige asserties werden gereduceerd tot 6, terwijl geïmpliceerde asserties toenamen tot 92.

Analyse van Resultaten:
De experimenten onthulden dat basismethoden vaak asserties genereren die ofwel in tegenspraak zijn met de specificatie of sterk afhankelijk zijn van implementatiespecifieke details (RTL) die niet in de natuurlijke taalspecificatie voorkomen. SpecAlign filtert deze tegenstrijdigheden effectief eruit. De toename in "Onbekend"-classificaties bij SpecAlign (bijvoorbeeld 376 voor APB) wordt geïnterpreteerd niet als een falen, maar als een meer conservatieve en accurate classificatiestrategie die implementatiespecifieke aannames scheidt van door de specificatie ondersteund gedrag. Dit onderscheid voorkomt het vals positief labelen van niet-ondersteund gedrag als "geïmpliceerd".

5. Betekenis en Claims

Het artikel beweert dat SpecAlign een schaalbare aanvulling biedt op traditionele formele verificatie. Door semantische correctheid te scheiden van RTL-bewijsresultaten, adresseert het de beperking dat formele verificatie alleen niet kan bepalen of een assertie het bedoelde gedrag dat in de specificatie wordt beschreven, vastlegt.

De auteurs benadrukken dat hoewel formele verificatie noodzakelijk is om te bewijzen dat asserties gelden op RTL, het ontoereikend is voor het evalueren van de kwaliteit van de intentie van de assertie. SpecAlign verbetert het vertrouwen in door LLM's gegenereerde asserties door:

1. Semantische inconsistenties te detecteren die formele tools mogelijk missen (bijvoorbeeld vacuüm waarheden).
2. Debugging-inspanningen te verminderen door tegenstrijdigheden te identificeren voordat RTL-simulatie of formeel bewijs plaatsvindt.
3. Een mechanisme te bieden om asserties iteratief te verfijnen zonder een golden-model te vereisen.

Het artikel concludeert bescheiden, met de opmerking dat hoewel het kader de uitlijning verbetert, toekomstig werk nodig is om classificatiemethodologieën te verfijnen, syntactische fouten beter te vangen en de aanpak uit te breiden naar andere taken voor hardwareontwerpsautomatisering, zoals RTL-generatie en debugging.