About / Advertise
Enligt experterna är det inte särskilt svårt att komma igång med statisk funktionell verifiering.Den stora skillnaden ligger i tänkesättet - i stället för att specificera ett antal indata och förväntade utdata som vid simulering så gäller det att översätta specifikationen till ett formellt språk, i praktiken en lista med egenskaper (property list).
Den första svårigheten - själva språket - är egentligen den enklaste. Visserligen varierar syntax och semantik en del, beroende på vilket verktyg och därmed vilket språk man använder. Men den som behärskar VHDL eller Verilog torde inte ha några svårigheter att sätta sig ini de extra språkkonstruktioner som krävs.
Aningen värre är det att formulera själva egenskaperna. Somliga är enkla, av typen "om a gäller så ska alltid b också gälla" eller "signalen c ska alltid vara onehot". Lite svårare att tänka ut är egenskaper av typen "om a inträffar, och samtidigt b inträffar så får c aldrig hända".
Lätt att skriva egenskaper
En av tjusningarna är att även tämligen komplexa egenskaper som sträcker sig över flera klockcykler kan formuleras ganska enkelt. Exempelvis kan man på en enda rad specificera att en tillståndsmaskin som går in i tillståndet S1 inom fem klockcykler måste gå till tillståndet S2, oavsett indata. Att med simulering bevisa att detta alltid gäller skulle - om det över huvud taget var möjligt - kräva en testbänk med många rader kod.
- Det här är inte särskilt svårt. Att skriva egenskaper är egentligen mycket lättare än att skriva testbänkar, säger Kenneth Larsen på Mentor Graphics.
- Det svåra är egentligen att skriva specifikationen. Om den är välgjord så är det inte alls komplicerat att översätta den till egenskaper. Men om specifikationen är slarvig eller gjord i efterhand som något slags dokumentation så hittar man ofta tvetydigheter och brister
i den. Och då blir det genast svårare, säger Jonas Nilsson på Hardi Electronics.
Hur vet man då att listan över egenskaper är tillräckligt uttömmande? Just det är själva knäckfrågan, det medger även företagen som säljer dessa produkter. Antalet egenskaper som måste beskrivas varierar också med tillämpningen - reguljära block kräver betydligt färre egenskaper än konstruktioner med många tillståndsmaskiner.
- En studie som Averant gjorde för något år sedan visade att det i snitt krävdes en egenskap för 2 till 5 rader RTL-kod för full verifiering. Sedan dess har språket förbättrats en aning, så idag skulle jag tro att man kan klara sig med hälften så många egenskaper, säger Jonas Nilsson.
När det gäller simulering finns gott om verktyg som indikerar hur väl en testbänk är skriven, och hur stor del av potentiella fel de täcker. Det finns också så kallade "lint checkers" som indikerar onödig kod i testbänkarna. För formell verifiering finns ännu inte särskilt många sådana verktyg.
Adam Edström
