Chipverificatie: hoe weet je zeker dat een chip doet wat hij moet doen?
Stel je voor dat een architect een gebouw van honderd verdiepingen ontwerpt, en pas na de bouw ontdekt dat de liften niet werken. Bij een chip is dat scenario nog veel duurder: als een fout pas opduikt nadat de chip in een fabriek is geproduceerd, ben je tientallen miljoenen euro's en maanden tijd kwijt om het opnieuw te doen. Chipverificatie is het geheel van technieken waarmee ingenieurs, voordat een chip daadwerkelijk gemaakt wordt, controleren of het ontwerp echt doet wat het moet doen.
Een chip zoals een processor of een grafische kaart bestaat tegenwoordig uit miljarden schakelingen (transistors) die samen miljoenen mogelijke toestanden en gedragingen kunnen vertonen. Een menselijke ontwerper kan onmogelijk met het blote oog zien of ergens een fout zit. Verificatie is daarom een apart vakgebied geworden, met eigen software, eigen specialisten en eigen methodes, dat draait om één simpele vraag: klopt het ontwerp met wat het hoort te doen, in alle situaties die zich kunnen voordoen?
Wat is het precies?
Een chip wordt eerst beschreven in een soort programmeertaal voor hardware, met namen als Verilog of VHDL. Dat heet RTL (register-transfer level): een tekstuele beschrijving van hoe data tussen geheugenelementen stroomt en welke logische bewerkingen daarbij gebeuren. Die RTL-beschrijving is het startpunt voor verificatie, nog ver voordat er ook maar één fysieke laag silicium wordt gemaakt.
De meest gebruikte techniek is simulatie: een softwaremodel van de chip wordt in een computer nagebootst, en er worden testsignalen ('testbenches') ingevoerd om te zien of de uitkomst klopt. Dit gebeurt vaak volgens een gestandaardiseerde aanpak genaamd UVM (Universal Verification Methodology), een verzameling herbruikbare bouwstenen voor testomgevingen, gebaseerd op de taal SystemVerilog.
Omdat je met simulatie nooit alle mogelijke combinaties van invoer kunt testen, bestaat er ook formele verificatie. Dit is een wiskundige aanpak: in plaats van duizenden losse tests te draaien, bewijst speciale software dat een bepaalde eigenschap (bijvoorbeeld 'dit geheugenadres wordt nooit twee keer tegelijk beschreven') voor alle mogelijke gevallen klopt, net zoals een wiskundig bewijs geldt voor alle getallen tegelijk in plaats van voor een paar voorbeelden.
Voor grotere ontwerpen is pure simulatie te traag. Dan wordt gebruikgemaakt van emulatie: speciale, extreem grote hardwaremachines die de chip nabootsen en die duizenden keren sneller zijn dan software-simulatie op een gewone computer, en van FPGA-prototyping, waarbij het ontwerp wordt geladen op een programmeerbare chip (FPGA) om er al bijna-echte software op te kunnen draaien.
Tot slot wordt bijgehouden hoeveel van het ontwerp en van de mogelijke situaties daadwerkelijk getest zijn: de zogeheten coverage (dekking). Pas als de coverage-doelen gehaald zijn, mag een team met vertrouwen zeggen dat de verificatie 'klaar' is en dat de chip naar de fabriek (het zogeheten tape-out) mag.
Wat wil men ermee bereiken?
Het belangrijkste doel is simpel: fouten vinden vóórdat de chip geproduceerd is. Het maken van de mallen (maskers) voor een geavanceerde chip kost al snel tientallen miljoenen euro's, en het hele fabricageproces duurt maanden. Een fout die pas na productie ontdekt wordt, betekent een kostbare 'respin': opnieuw ontwerpen, opnieuw produceren, opnieuw maanden wachten.
Daarnaast speelt veiligheid een steeds grotere rol. Chips zitten tegenwoordig in auto's, medische apparatuur en vliegtuigen, waar een defect niet alleen geld kost maar mensenlevens in gevaar kan brengen. Voor dit soort toepassingen gelden strenge veiligheidsnormen die uitgebreide verificatie verplicht stellen.
Verificatie is ook een kwestie van vertrouwen in de toeleveringsketen: een chipontwerper moet erop kunnen vertrouwen dat een stukje herbruikbare hardware ('IP-block') dat wordt ingekocht, ook echt doet wat de leverancier belooft. Tot slot is er een economisch motief: in veel moderne chipprojecten kost verificatie inmiddels meer tijd en mankracht dan het eigenlijke ontwerpen, simpelweg omdat de complexiteit van chips sneller groeit dan de mogelijkheden om ze te testen.
Voorbeelden uit de praktijk
Een van de bekendste waarschuwende voorbeelden is de Pentium FDIV-bug uit 1994: Intel's eerste Pentium-processor bevatte een subtiele fout in de deel-eenheid voor kommagetallen, die in zeldzame gevallen een licht verkeerd antwoord gaf. De fout werd ontdekt door een wiskundige buiten Intel, leidde tot een kostbare terugroepactie en wordt algemeen gezien als een belangrijke aanleiding voor de chipindustrie, en Intel in het bijzonder, om zwaar te investeren in formele verificatiemethoden voor rekenkundige schakelingen.
Een actueler voorbeeld is OpenTitan, een open-source project voor een zogeheten 'silicon root of trust'-chip: een klein, extra beveiligd chipje dat controleert of de rest van een computer of server nog te vertrouwen is. Het project werd in 2019 gelanceerd door het Britse bedrijf lowRISC, met steun van onder meer Google, en combineert klassieke UVM-simulatie met open-source formele verificatietools uit de Yosys-toolketen.
Binnen de open RISC-V-processorarchitectuur is riscv-formal een bekend hulpmiddel: een open-source raamwerk, ontwikkeld door de Duitse ingenieur Clifford Wolf, waarmee automatisch gecontroleerd kan worden of een zelfgebouwde RISC-V-processorkern zich werkelijk aan de officiële specificatie houdt.
In de wereld van grote chipontwerpers zoals ARM wordt formele verificatie onder meer ingezet om complexe communicatieprotocollen tussen processorkernen te controleren, zoals protocollen die ervoor zorgen dat verschillende rekenkernen altijd dezelfde, actuele versie van gegevens in het geheugen zien (cache-coherentie). Dit soort eigenschappen is met gewone simulatie nauwelijks volledig te testen, wat formele technieken hier bijzonder waardevol maakt.
Tot slot is er de auto-industrie: onder de internationale veiligheidsnorm ISO 26262 voor elektronica in voertuigen moeten fabrikanten zoals NXP en Infineon uitgebreid aantonen dat hun chips, bijvoorbeeld voor remsystemen of stuurbekrachtiging, geverifieerd zijn tegen zowel functionele fouten als willekeurige hardwarestoringen.
Hoe ver is de techniek?
Chipverificatie is een volwassen vakgebied met decennia aan ervaring, maar het staat tegelijk onder toenemende druk. Het aantal transistors op een chip blijft groeien, en daarmee groeit het aantal mogelijke toestanden van een ontwerp veel sneller dan de rekenkracht die beschikbaar is om al die toestanden te controleren. Dit staat bekend als het probleem van de 'toestandsexplosie', en het is de reden waarom formele verificatie meestal alleen wordt toegepast op kleinere, kritieke onderdelen van een chip in plaats van op de volledige chip tegelijk.
Simulatie blijft de werkpaard-techniek, maar wordt voor grote systemen-op-een-chip steeds vaker aangevuld of vervangen door emulatie en FPGA-prototyping, juist omdat pure software-simulatie te traag is geworden voor moderne ontwerpen die complete besturingssystemen moeten kunnen draaien tijdens het testen.
Een opkomende ontwikkeling is het gebruik van machine learning om automatisch interessante testgevallen te genereren en om sneller de laatste, moeilijk te bereiken coverage-doelen te halen. Dit staat nog in een relatief vroeg stadium en vervangt de bestaande methodes niet, maar wordt door meerdere grote leveranciers actief onderzocht en in producten geïntegreerd.
Het is belangrijk eerlijk te zijn over de grenzen van chipverificatie: het is gericht op het aantonen dat een chip zich functioneel gedraagt zoals gespecificeerd. Bepaalde beveiligingsproblemen, zoals de bekende Meltdown- en Spectre-kwetsbaarheden die in 2018 wereldwijd nieuws waren, ontstaan niet doordat een chip zich anders gedraagt dan gespecificeerd, maar doordat het spectrum van 'ongewenst gedrag' (in dit geval: informatie lekken via subtiele tijdsverschillen) niet in de oorspronkelijke specificatie was meegenomen. Dat laat zien dat verificatie zo goed is als de eisen waartegen getest wordt, en dat nieuwe soorten dreigingen voortdurend nieuwe verificatiemethodes vereisen.
Wie werken eraan?
Het gereedschap voor chipverificatie wordt grotendeels geleverd door een klein aantal gespecialiseerde bedrijven in elektronische ontwerpautomatisering (EDA), waarvan Synopsys en Cadence (beide Verenigde Staten) en Siemens EDA (voorheen Mentor Graphics, nu onderdeel van het Duitse Siemens) de grootste zijn.
Vrijwel elk groot chipbedrijf heeft eigen, vaak grote, verificatieteams: Intel, AMD, NVIDIA en Qualcomm in de Verenigde Staten, ARM in het Verenigd Koninkrijk, en in Europa onder meer NXP en Infineon, met sterke vestigingen in Nederland en Duitsland. Ook Aziatische spelers zoals TSMC (Taiwan, als producent) en Samsung (Zuid-Korea) zijn nauw betrokken, al ligt hun rol meer bij fabricage dan bij ontwerpverificatie zelf.
Academisch onderzoek naar formele verificatiemethoden gebeurt onder meer aan Amerikaanse universiteiten als MIT en Stanford, en in Europa aan instellingen zoals ETH Zürich en de universiteit van Cambridge. Het open-source RISC-V-ecosysteem, aangestuurd door de non-profitorganisatie RISC-V International, en het Britse bedrijf lowRISC spelen een steeds grotere rol bij het toegankelijk maken van professionele verificatietechnieken buiten de grote, gesloten chipbedrijven om.
Ten slotte is India in de afgelopen jaren uitgegroeid tot een van de grootste centra ter wereld voor verificatie-ingenieurs, met grote vestigingen van vrijwel alle bovengenoemde bedrijven in steden als Bangalore en Hyderabad.