Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

Dit artikel presenteert een schaalbare methodologie voor het formeel verifiëren van drijvende-kommaberekeningen via directe RTL-tot-RTL modelchecking, waarbij een verdeel-en-heerst-strategie wordt gecombineerd met door AI gegenereerde eigenschappen en menselijke feedback om de dekking en efficiëntie te maximaliseren.

De kern

De "Wiskundige Dubbelcheck": Hoe Computers Zorgen Dat Hun Rekenen Perfect Is

Stel je voor dat je een superkrachtige rekenmachine bouwt die niet alleen optelt en aftrekt, maar ook met heel kleine, ingewikkelde getallen werkt (zoals 3,14159265...). In de wereld van computerchips noemen we dit een "Floating Point Unit" (FPU). Het probleem is: als deze chip één klein foutje maakt, kan dat leiden tot rampen. Denk aan een raket die verkeerd landt, of een medische machine die de verkeerde dosis berekent.

De auteurs van dit paper (Hansa, Vaisakh en Deepak) hebben een nieuwe manier bedacht om te controleren of zo'n rekenmachine perfect werkt. Hier is hoe ze dat doen, vertaald naar alledaagse taal:

1. Het Probleem: De Vertaalprobleem

Vroeger controleerden ingenieurs hun chipontwerpen door ze eerst om te zetten naar een simpele C-programma (een soort "hoog niveau" taal) en die te vergelijken met de echte chip.

• De analogie: Dit is alsof je een heel gedetailleerd architecturaal plan voor een brug (de chip) vertaalt naar een schets op een napkin (het C-programma) en dan zegt: "Als de schets klopt, klopt de brug wel."
• Het risico: Bij het vertalen gaan details verloren. De brug kan toch instorten, terwijl de schets er perfect uitzag.

2. De Oplossing: De "Tweeling"-Check

In plaats van te vertalen, vergelijken ze de echte chipontwerp (RTL) direct met een "Gouden Referentie" (een perfecte, maar langzamere versie van hetzelfde ontwerp).

• De analogie: Stel je twee identieke tweelingen voor. De ene is de echte, snelle rekenmachine (de implementatie). De andere is een langzame, maar 100% perfecte rekenmachine (de gouden referentie).
• De test: Ze laten de tweelingen exact dezelfde ingewikkelde sommen doen. Als ze op het eind een ander antwoord geven, is er een fout. Ze kijken niet naar de schets, maar vergelijken de twee broers direct.

3. De Strategie: De Taak Opsplitsen

Een hele complexe rekenmachine is te groot om in één keer te controleren. Het is alsof je probeert te bewijzen dat een heel groot kasteel veilig is door in één keer naar het dak te kijken.

• De aanpak: Ze splitsen de taak op in kleine kamers (modules). Eerst kijken ze alleen naar de "mantissa" (het deel van het getal dat de cijfers bepaalt), en daarna naar de "optelling en afronding".
• De analogie: Het is alsof je een grote puzzel in stukjes verdeelt. Je controleert eerst of de randstukken passen, dan of de binnenkant klopt. Als een stukje niet past, zie je direct waar het misgaat, in plaats van door de hele puzzel te zoeken.

4. De Nieuwe Hulp: De AI-Assistent

Dit is het spannendste deel van het paper. Het schrijven van alle regels om te controleren of de puzzelstukjes passen, is veel werk. De auteurs hebben dus een team van AI-agenten ingeschakeld.

• Hoe het werkt:
  1. De Planner: Een AI leest het ontwerp en maakt een plan: "We moeten controleren of de cijfers kloppen."
  2. De Schrijver: Een andere AI schrijft de controle-regels (in een speciale taal voor computers).
  3. De Critic: Een derde AI kijkt of de regels logisch zijn.
  4. De Mens (HITL): Als de AI vastloopt of twijfelt, komt een menselijke expert tussenbeide om de AI te corrigeren.
• De uitkomst: De AI schrijft snel veel regels, maar soms zijn ze dubbelop of niet helemaal goed. Met een beetje hulp van een mens (de "Human-in-the-Loop") worden ze slim en efficiënt. Het is alsof je een stagiair hebt die snel veel werk doet, maar die een meester moet vragen om de laatste hand te leggen.

5. De Test: "Stress Test"

Om te zien of hun methode echt werkt, hebben ze expres fouten in de chip gezet (zoals een verkeerde schakelaar of een getal dat verkeerd wordt afgerond).

• Het resultaat: Hun methode vond alle fouten. Zelfs de fouten die de AI-assistent had gemaakt, werden opgespoord.
• De les: Als je de AI alleen laat werken zonder menselijke controle, maakt hij soms fouten of schrijft hij te veel onnodige regels. Maar met een mens die meekijkt, wordt het systeem razendsnel en extreem betrouwbaar.

Conclusie

Kortom: Deze wetenschappers hebben bewezen dat je de beste manier om een computerchip te controleren, is door hem direct te vergelijken met een perfecte kopie, zonder tussenstapjes. En als je daarbij slimme AI-assistenten gebruikt die door mensen worden begeleid, gaat het niet alleen sneller, maar is het resultaat ook veiliger dan wanneer je het alleen met de hand doet.

Het is als het bouwen van een raket: je vertrouwt niet alleen op de tekeningen, je bouwt een perfecte tweeling, laat ze samen vliegen, en gebruikt een robot-assistent die door een ervaren piloot wordt gecontroleerd om zeker te weten dat alles perfect werkt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Formal Verification of Floating Point Arithmetic" in het Nederlands.

Titel: Formele verificatie van drijvende-kommaberekeningen (Formal Verification of Floating Point Arithmetic)

Auteurs: Hansa Mohanty, Vaisakh Naduvodi Viswambharan, Deepak Narayan Gadde (Infineon Technologies)
Publicatie: 37e IEEE International Conference on Microelectronics (ICM), 2025.

---

1. Het Probleem

De verificatie van hardware-ontwerpen, en specifiek van drijvende-kommabewerkingen (Floating-Point Units - FPUs), blijft een uitdaging vanwege de complexe interactie tussen discrete besturingslogica en rekenkundige datapaden.

• Uitdagingen: FPUs moeten voldoen aan strikte IEEE-754-standaarden en omvatten complexe bewerkingen zoals exponentuitlijning, normalisatie en afronding. Dit leidt tot randgevallen (zoals denormaliseerde operanden, overflow en precisieverlies) die moeilijk te testen zijn.
• Beperkingen van bestaande methoden: Traditionele benaderingen vertrouwen vaak op hoog-niveau C-modellen voor equivalentiecontrole tegen RTL-ontwerpen (Register Transfer Level). Dit introduceert echter:
  • Abstractiegaten: Semantische verschillen tussen C-code en hardware-executie.
  • Schalingsproblemen: Moeilijkheden bij het toepassen op datapad-intensieve RTL-ontwerpen.
  • Onderhoud: Grote inspanning voor het handhaven van de vertaling tussen modellen.

2. Methodologie

Het artikel presenteert een schaalbare methodologie voor formele verificatie die directe RTL-naar-RTL modelchecking toepast, zonder afhankelijkheid van hoog-niveau software-abtracties.

• Directe Vergelijking: De implementatie (RTL) wordt direct vergeleken met een gouden referentiemodel (eveneens in SystemVerilog), wat zorgt voor bit-accurate conformiteit.
• Hiërarchische Decompositie (Divide-and-Conquer): Het ontwerp wordt opgesplitst in modulaire fasen om de complexiteit te verminderen en de "cone of influence" (COI) te verkleinen. Voor een floating-point adder worden twee fasen onderscheiden:
  1. Mantisse-uitlijning: Het verschuiven van de kleinere mantisse op basis van het exponentverschil.
  2. Optellen en Afronden: Het optellen van de uitgelijnde mantissen, gevolgd door normalisatie en afronding.
• Theorema's en Lemma's: De correctheid wordt bewezen via een hoofdtheorema (Resultaat-equivalentie) dat wordt ondersteund door tussenliggende lemma's en helper-asserties voor elke fase.
• CEX-geleide verfijning: Als de tool een tegenvoorbeeld (Counterexample - CEX) genereert, wordt dit gebruikt om fouten in de implementatie of de eigenschappen te lokaliseren en te corrigeren.
• Agentic AI voor Eigenschapsgeneratie: Een multi-agent systeem (met LLM's zoals GPT-5 en Llama3.3) wordt ingezet om SystemVerilog Assertions (SVAs) te genereren vanuit natuurlijke taal. Dit proces omvat:
  • Planning: Een Lead Agent creëert een verificatieplan.
  • Generatie & Kritiek: Agents genereren eigenschappen en evalueren deze op logica en dekking.
  • Human-in-the-Loop (HITL): Menselijke experts geven feedback om ambiguïteiten op te lossen en de eigenschappen te verfijnen.

3. Belangrijkste Bijdragen

1. RTL-naar-RTL Modelchecking: Een methode die C-modellen elimineert en directe verificatie tegen een gouden RTL-referentie mogelijk maakt.
2. Eigenschapsgedreven Decompositie: Een gestructureerde aanpak die het ontwerp opsplitst in verifieerbare fasen, wat de bewijscomplexiteit verlaagt.
3. Foutdetectie en -oplossing: Het succesvol identificeren en oplossen van implementatiefouten (zoals verkeerde operandselectie en exponent-mismatch) via CEX-analyse.
4. Foutinjectie: Systematische injectie van fouten in de datapad om de robuustheid van de verificatie te testen. Alle injecteerde fouten werden gedetecteerd.
5. AI-gestuurde Verificatie: Een vergelijkende studie tussen handgeschreven eigenschappen en AI-generatie, waarbij wordt aangetoond dat HITL-refinement cruciaal is voor de kwaliteit van AI-generatie.

4. Resultaten

De methodologie werd getest op een open-source floating-point adder (SystemVerilog) met de Cadence Jasper Formal Verification Platform.

• Foutdetectie: De methode ontdekte en corrigeerde fouten in de operand-selectie en inverteringslogica van de mantisse, evenals problemen met exponent-gedrag in de optel-fase.
• Foutinjectie: Alle 8 geinjecteerde fouten (4 in de uitlijnfase, 4 in de optel/afrond-fase) werden succesvol gedetecteerd, wat de gevoeligheid van de eigenschappen aantoont.
• Dekkingsanalyse (Coverage):
  • RTL-naar-RTL met Referentie: Handgeschreven eigenschappen bereikten 98,42% formele dekking met slechts 2 eigenschappen (0,073s bewijstijd).
  • AI-generatie: Zonder menselijke input (HITL) genereerden LLM's meer eigenschappen (7-15) met redundante intenties en langere bewijstijden. Met HITL-refinement konden AI-modellen (zoals GPT-5) echter even efficiënt worden: GPT-5 bereikte vergelijkbare dekking met slechts 3 eigenschappen en een bewijstijd van 1,318s.
  • Standalone Verificatie (zonder Referentie): Zonder gouden referentiemodel daalde de dekking aanzienlijk (bijv. 62-90%) en nam het aantal onbereikbare items toe. Dit vereiste aanzienlijke menselijke input om de micro-architecturale beperkingen correct te definiëren.

5. Betekenis en Conclusie

Dit onderzoek toont aan dat directe RTL-naar-RTL modelchecking, ondersteund door een hiërarchische decompositiestrategie, superieur is aan traditionele C-gebaseerde flows voor de verificatie van complexe datapaden.

De integratie van Agentic AI voor het genereren van formele eigenschappen is veelbelovend, maar vereist menselijke begeleiding (HITL) om redundantie te elimineren en de juiste micro-architecturale beperkingen te definiëren. Zonder een gouden referentiemodel is AI nog niet in staat om de volledige bereikbare toestandsruimte van drijvende-kommabewerkingen adequaat te construeren.

De studie biedt een fundament voor schaalbare, AI-ondersteunde formele verificatie, waarbij de toekomstige uitdaging ligt in het verbeteren van de extractie van micro-architecturale intenties om de menselijke inspanning verder te minimaliseren.