Formell verifiering ger kretsar med högre kvalitet. Det menar två konsulter som testat marknadens verktyg för formell verifiering.
Simulering och emulering i all ära. Men om man verkligen vill verifiera konstruktionen fullständigt är formell verifiering ett bättre alternativ.
- Formell verifiering är användbart redan idag. Men man måste veta hur verktygen fungerar för att kunna anpassa koden, säger Kenneth Östberg som är konsult på Carlstedt VHDL Design i Göteborg.
Utvärderade två fabrikat
Carlstedt och Stockholmsföretaget Logikkonsult NP har tillsammans utvärderat verktyg för formell verifiering från Chrysalis Symbolic Design och Abstract Hardware. Bakom studien stod FMV.
En befintlig 60 000-grindarskrets, som skulle modifieras för Ericsson Microwaves räkning, fick agera försökskanin.
Konsultduon testade så kallade ekvivalenstestare där man försöker bevisa att två olika beskrivningar av konstruktionen har exakt samma funktion. Man jämförde VHDL-beskrivningar på registernivå med varandra, mellan grind- och registernivåbeskrivningar plus mellan beskrivningar på grindnivå.
Slutsatsen blev att formell verifiering sparar tid, eftersom man minskar behovet av traditionell simulering. Kenneth Östberg tycker att metoden är särskilt användbar på grindnivå.
- Ofta måste man införa buffrar och rättningar i nätlistan sent i projekten. Då har man bråttom och hinner inte simulera konstruktionen fullständigt. Men med formell verifiering vet man ändå att man har gjort en fullständig test.
På minussidan nämner han det höga priset och att det krävs en hel del utbildning. Men fördelarna överväger helt klart:
- Kretsens kvalitet ökar eftersom man testar saker man aldrig kommer åt med en simulator, slår han fast.