Formella verifieringsmetoder kan vara ett alternativ till simulering

Formella, matematiska metoder är ett lovande alternativ till simulering för verifiering av stora kretskonstruktioner. I teorin är metoden överlägsen, men verktygen är långt ifrån färdiga.

Handen på hjärtat. Är asicens testvektorer verkligen heltäckande? Och hinner kretsen simuleras fullständigt utan att projektets tidsplan spricker?

Få konstruktörer vågar svara ja på sådana frågor. Att verifiera konstruktionen med hjälp av simulering, som fortfarande är den vedertagna metoden, blir nämligen allt knivigare när kretsarnas grindantal ökar samtidigt som ledtiderna krymper.

En av de stora stötestenarna är att det tar för lång tid att skapa tillräckligt många testvektorer. Men även om man kunde skapa alla dessa vektorer så skulle simuleringstiden bli orimligt lång. Det räcker inte ens att använda snabba cykelbaserade simulatorer eller hårdvaruacceleratorer.

Då är formell - matematisk - verifiering ett lovande alternativ. Testvektorer behövs inte och själva verifieringen går mycket snabbt. På några minuter klarar ett formellt verktyg uppgifter som tar timmar för simulatorn, säger entusiasterna. Kretsen verifieras dessutom för alla möjliga tillstånd och indata, till skillnad från simulatorer som bara testar de relativt få situationer som täcks av testvektorerna.

Två huvudgrupper

Efterfrågan på dessa verktyg ökar och företag som Compass, Chrysalis och Abstract Hardware har vissa framgångar med sina produkter i denna nisch. Även IBM och Lucent, före detta AT&T, är aktiva inom området.

De formella verktygen kan delas in i två huvudgrupper; ekvivalenstestare och modelltestare.

Ekvivalenstestarna är vanligast och kanske lättast att begripa sig på. Konstruktören skapar först en så kallad guldmodell av konstruktionen. Denna guldmodell, som skall användas som referens, är ofta en Verilog- eller VHDL- beskrivning på beteendenivå som simuleras grundligt på traditionellt sätt.

Ekvivalenstestaren tas fram först när beskrivningen på registernivån är klar. Verktyget bygger då matematiska modeller, alltså ekvationer, av såväl guldmodellen som registernivåbeskrivningen och försöker bevisa att ekvationerna från de båda beskrivningarna har exakt samma funktion. Även grindnivåbeskrivningen och senare nätlistor jämförs sedan allt eftersom med tidigare beskrivningar. På så vis garanterar man att inga fel införs under arbetets gång.

Metoden har en uppenbar nackdel. Allt står ju och faller med att guldmodellen verkligen är felfri. Ekvivalenstestaren garanterar annars att felen bevaras ända fram till färdigt kisel - en mardröm för varje konstruktör. Många menar därför att dessa verktyg enbart bör användas i slutet av konstruktionsarbetet efter att konstruktionen verkligen är grundligt verifierad.

Från början till slut

En modelltestare kan däremot användas under hela arbetsflödet, från beteendenivå till slutgiltig nätlista. Modelltestaren kontrollerar att beskrivningen har det önskade logiska beteendet utifrån ett antal frågor som användaren ställer.

Frågorna kan vara på ganska hög nivå, exempelvis "Kommer en enhet som begär att få använda databussen så småningom få tillträde till denna buss?"

Lika viktigt är att verktyget används för kontroll av att inget oönskat kan inträffa. Med frågan "Kan signalerna buffer_write och buffer_full vara sanna samtidigt?" testas exempelvis att det inte går att skriva till en buffert som redan är full.

För att ställa lämpliga frågor måste man veta exakt vad kretsen skall göra och inte göra. Men själva implementationen behöver man däremot inte vara så insatt i. Verifieringen kan alltså göras av någon annan än konstruktören. Det är en stor fördel, då man ju lätt blir blind för sina egna fel.

Tyvärr är verktygen för modelltestning långt ifrån färdigutvecklade. De som finns på marknaden har bara börjat nosa på de möjligheter som finns i teorin.

Varken ekvivalenstestare eller modelltestare tar hänsyn till timingen. Formell verifiering kan därför med fördel användas tillsammans med statisk timing- analys.

CHARLOTTA von Schultz