Lars Philipson rekommenderar denna bok om formell verifiering: Principles of Verifiable RTL Design, av Lionel Bening och Harry Foster, utgiven av Kluwer, år 2000.

För några år sedan var det en allmänt känd sanning att verifieringen av en asic kunde ta upp till halva konstruktionstiden. Detta ansågs då vara ett stort problem.

Sedan dess har det bara blivit värre. Idag är det inte ovanligt att 70 eller 80 procent av konstruktionstiden går till verifiering. Trots snabbare simulatorer, hårdvaruemulatorer, automatiska testbänksgeneratorer, feltäckningsanalysatorer och andra nya simuleringshjälpmedel så växer alltså problemet.

Entusiaster i verktygsbranschen har under de senaste åren med allt större emfas hävdat att lösningen heter formell verifiering. Teorierna är inte nya - de har varit kända inom akademin sedan 1960-talet. Det är dock bara några år sedan som de första användbara kommersiella verktygen lanserades.

- Jag började titta på formella verktyg 1989. Då var de inte användbara. Sedan dess har jag följt utvecklingen, och förra året kunde jag konstatera att verktygen mognat, säger Lars Philipson, professor i datorteknik i Lund.

Visar att specifikationen uppfylls

Med formella, matematiska metoder kan man visa att en konstruktion alltid uppfyller specifikationen. Man gör detta genom att bevisa att en serie villkor alltid är uppfyllda - och ännu bättre - man kan bevisa att vissa villkor aldrig kommer att uppfyllas.

Sålunda går det att få hundraprocentig feltäckning, och allt detta utan att skriva en enda testvektor. Just denna tekniken kallas statisk funktionell verifiering, alternativt modellkontroll (model checking).

- Största poängen är att man kan veta säkert att hela konstruktionen är verifierad. Hur mycket man än simulerar kan man aldrig bli lika säker på det - man kan aldrig vara säker på att det inte finns något hörnfall som simuleringen missar, säger Jonas Nilsson på Hardi Electronics som säljer denna typ av verktyg.

En variant av formell verifiering kallas ekvivalenskontroll. Denna går ut på att försäkra sig om att två beskrivningar av samma konstruktion garanterat ger samma funktion - att de är funktionellt ekvivalenta.

Exempelvis kan man visa att en beskrivning på grindnivå är funktionellt densamma som motsvarande beskrivning på registernivå, eller att kunna
visa att funktionen på grindnivå är densamma före och efter inläggning av testslingor.

- Vi har använt ekvivalenskontroll sedan 1997. Då var vi troligen först att använda metoden inom Ericsson, säger Hans-Olov Eriksson, asicansvarig på Ericsson Radio Systems.

Numera tillämpar Ericsson ekvivalenskontroll standardmässigt på alla asicar. Man använder ett flertal verktyg från olika leverantörer.

- Att vi började använda ekvivalenskontroll var naturligtvis kopplat till att asicleverantörerna vid den tiden började stödja statisk-timing sign-off. Genom att verifiera nätlistan formellt från RTL till grindnivå så kunde vi dra ner på tidskrävande sign-offsimuleringar på grindnivå, säger Eriksson.

Hans grupp jobbar även med fysisk konstruktion och layout, där slutgiltig timing (timing closure) och layoutoptimering är viktiga delar. Då ändras också nätlistan på flera sätt.

- Ekvivalenskontroll ger oss då formellt bevis på att den slutgiltiga nätlistan och originalnätlistan från syntesverktyget är logiskt ekvivalenta, säger Eriksson.

Utanför Ericsson är bilden betydligt mer blandad - även denna tämligen enkla form av formell verifiering ses alltjämt som något främmande av många konstruktörer.

Ingen ny kunskap

Ekvivalenskontroll är alltså ett accepterat och näst intill ovärderligt verktyg på vägen från registernivå till sign-off. Men metoden ger ingen ny kunskap om beskrivningen på registernivå. Något raljant uttryckt så kan man med ekvivalenskontroll garantera att fel i RTL-koden fortplantas till grindnivån.

Ska man formellt försäkra sig om korrekt RTL-kod så krävs modellkontroll eller statisk funktionell verifiering.

Ändå är acceptansen inte alls densamma för dessa verktyg. Trots att metoden ger enorma möjligheter till tidsbesparing och försäkring om att
en konstruktion verkligen är korrekt så finns inte särskilt många användare.

- Vi har utvärderat den typen av verktyg i flera år för användning på Ericssons egenutvecklade DSP-kärnor. Problemet har varit att verktygen har haft inbyggda kapacitetsbegränsningar. Det har helt enkelt varit omöjligt att verifiera mer
än ett par tusen grindar formellt, säger Hans-Olov Eriksson och påpekar att dessa grundläggande kapacitetsproblem måste lösas innan metoden kan slå igenom.

- För närvarande utvärderar vi ett nytt modellkontrollsverktyg, och resultaten så här långt ser lovande ut, säger han.

Ett annat skäl till att genombrottet dröjer är att de verktyg som finns på marknaden kommer från mindre företag som kanske inte har samma acceptans bland konstruktörerna som jättarna i verktygsbranschen. Leverantörer som Verplex, Averant, Real Intent och Valiosys har helt enkelt inte samma tyngd som Mentor Graphics, Synopsys och Cadence även om deras produkter i just denna nisch kan vara mer avancerade.

Mentor Graphics säljer idag ett verktyg för ekvivalenskontroll. Men man har jobbat på ett verktyg för modellkontroll i några år.

- Vi kommer under året att lansera ett verktyg som kan hantera block om flera hundratusen grindar, säger Kenneth Larsen, marknadschef för Mentors formella verktyg, som dock inte vill bekräfta huruvida lanseringen kommer redan på mässan Dac i juni.

Nytt sätt att tänka

Ett annat skäl är att modellkontroll innebär ett nytt sätt att tänka, vilket ju alltid är en tröskel att ta sig över. Konstruktörerna slipper skriva testvektorer, men måste å andra sidan formulera sin specifikation tydligare, och dessutom skriva ett antal "properties", en lista med egenskaper som formellt beskriver konstruktionen. Dessa måste dessutom ofta skrivas i något eget språk.

Det handlar alltså om en förändrad metodik, vilket många projektansvariga ryggar för eftersom det upplevs som ökat risktagande. Behovet finns dock, och även på mindre företag överväger man att börja med tekniken.

Ett exempel är Xelerated Packet Devices, där man inte använt formella metoder till sin första asic.

- Vi håller på att se över verifieringsansatsen för vårt andra kretsprojekt. Helt klart kommer vi att vilja biffa upp verifieringsstrategin för detta chips som har ett mer svårkaraktäriserat dynamiskt beteende, säger utvecklingschefen Joachim Roos.

Få investeringar

Den rådande konjunkturen gör förstås också att investeringsviljan överlag är minst sagt sval just nu.

- Alla vi pratar med är intresserade, och säger att detta säkert är något för framtiden. Men få vill satsa idag - det finns helt enkelt inga pengar, säger Jonas Nilsson på Hardi.

- Egentligen är det konstigt, för ett enda oupptäckt fel i en asic kostar mycket mer än att investera i de här mer robusta metoderna, säger han.

Det är inte heller särskilt lätt att hitta kunskap och kompetens för den som vill börja med formell verifiering. Någon akademisk undervisning finns knappt i Sverige. Närmast är nog Chalmers där formell verifiering ingår i föreläsningarna i de VHDL-kurser som ges i grundutbildningen för civilingenjörer.

- Vi planerar att ha laborationer nästa år, säger Sverker Steen på Chalmers.

Den som vill förkovra sig i ämnet är annars hänvisad till verktygsleverantörernas seminarier eller till självstudier. Det är alltså inte så konstigt att formella metoder inte slår igenom så snabbt.

- Erfarenhetsmässigt tar den här typen av förändringar lång tid. Jag skulle tro att det tar tio år innan modellkontroll slår igenom. Det tog ju 20 år att etablera konstruktion med tillståndsmaskiner, säger professor Lars Philipson i Lund.

Adam Edström