About / Advertise
Tyska Onespin Solutions har lanserat ett verktyg för formell verifiering som man hävdar löser många av de problem som tekniken hittills förknippats med, utan att kompromissa om resultatet.
Riskfri återanvändning av IP-block - det är ett av de viktigaste målen för tyska Onespin Solutions, en avknoppning från Infineon och Siemens. Ska processorkärnor och liknande kunna användas i system på kisel så måste man kunna verifiera att de verkligen fungerar som tänkt. Att hitta buggar och tvingas göra om kislet är helt enkelt för dyrt - bara maskerna kan kosta flera miljoner dollar.Dagens metoder, som simulering, automatisk testbänksgenerering och regressionstester kan aldrig ger denna garanti, trots att verifiering alltjämt står för 50-70 procent av tidsåtgången och kostnaden för ett konstruktionsprojekt. Formella, matematiska metoder har länge pekats ut som svaret, men verktygen har ofta ansetts svåra att använda och de har inte klarat särskilt stora konstruktioner. Undantaget är enklare så kallade ekvivalenskontroller, som formellt visar att en konstruktion på grindnivå har samma funktion som beskrivningen på registernivå (RTL).
Det Onespin nu gjort är att ta ekvivalenskontrollen till en högre abstraktionsnivå. Med det statiska formella verifieringsverktyget 360 MV, Module Verifier, kan användaren garantera att en beskrivning på transaktionsnivån är funktionellt överensstämmande med beskrivningen på RTL-nivå. Konsekvensen blir att konstruktörer kan ta beskrivningar av IP-block, para ihop dem och deras funktioner, och få en hundraprocentig garanti att de i praktiken fungerar på samma sätt som beskrivet på transaktionsnivån. Man kan också garantera att varje modul i ett IP-block är funktionellt buggfritt.
En stor poäng är att användaren får visshet om att varje del av konstruktionen verkligen är genomsökt av verktygen, och att det inte ens i teorin kan finnas buggar kvar. ”Verktyget avgör bortom all tvivel att verifieringen är komplett”, skriver Onespin i ett pressmeddelande.
Verktyget har använts med framgång i skarpa projekt, På Infineon har man verifierat en protokollprocessor kallad PPv2, med gott resultat. På 40 procent mindre tid än man tidigare använt i liknande, simuleringsbaserade verifieringar så hade man hittat alla teoretiskt tänkbara buggar. På företaget Dice använde man verktyget på en basbandsprocessor efter simuleringsprocessen, och hittade då 15 ytterligare buggar. Siemens har använt verktyget till två komplexa asicar med fyra miljoner grindar vardera, och hävdar att metoden var billigare och gav högre kvalitet än alla andra verifieringsmetoder man testat.
Verktyget klarar konstruktioner upp till ett par hundra tusen rader kod på RTL-nivå. Det kan användas med marknadens befintliga verktyg och kräver enligt företaget ingen ändring i konstruktionsflödet. Produktiviteten som Onespin anger ligger mellan 2000 och 4000 fullt verifierade rader kod på registernivå per ingenjörsmånad.
