About / Advertise
Ekvivalenskontroll, statisk funktionell verifiering, halvformella verktyg och bevismotorer attackerar verifieringsproblemet på olika sätt.
Ekvivalenskontroll (equivalence checking) är den enklaste formen av formell verifiering. Dessa verktyg kan visa att två beskrivningar av en konstruktion, exempelvis på registernivå och grindnivå, är funktionellt ekvivalenta. Den här typen av verktyg säljs av de flesta stora verktygstillverkare som Mentor Graphics, Cadence och Avant, samt av flera mindre företag.Modellkontroll (model checking) även kallad statisk funktionell verifiering, är nästa steg. Metoden går ut på att utifrån specifikationen formulera en serie egenskaper (properties) som konstruktionen ska uppfylla. Om listan över egenskaper görs rätt och tillräckligt uttömmande kan man bevisa att konstruktionen alltid och utan undantag följer specifikationen. Några användbara fullfjädrade verktyg för modellkontroll finns veterligen ännu inte.
Däremot finns flera verktyg för så kallad egenskapskontroll (property checking), en förenklad form av modellkontroll. Averant, Verplex, Valiosys och Real Intent är fyra företag i denna nisch. Averant utmärker sig här genom att företagets verktyg klarar både VHDL och Verilog, medan de övriga enbart hanterar Verilog.
Ett annat sätt att attackera verifieringsproblemet är med så kallade halvformella (semiformal) verktyg. Dessa applicerar modellkontroll på konstruktionen, men när ekvationerna blir för komplexa och körtiderna för långa så tar de till simulering för de sista delarna. Företaget 0-in är kanske mest känt i denna nisch, men även Avant, Verplex, Real Intent och @HDL marknadsför verktyg som kallas halvformella.
Försöker standardisera
Alla verktyg för modellkontroll kräver ett eget språk för formuleringen av egenskaperna. Här pågår försök till standardisering inom organisationen Accellera. Fyra kandidater finns, ett vardera från Motorola, Intel och IBM samt Temporal E från verktygsleverantören Verisity. Troligen kommer dock standardiseringen att ta många år innan den är klar, och under tiden kan mycket väl något verktyg ha etablerat sig som marknadsledande och därmed dess språk som defacto-standard.
Uppräkningen av formella verktyg blir inte komplett utan att nämna så kallade bevismotorer, där svenska Prover är en aktör. En bevismotor löser de komplexa matematiska beräkningarna för formella verifieringsverktyg. De är inte särskilt användbara fristående. Prover och dess konkurrenter har i stället ambitionen att sälja bevismotorer till andra verktygsleverantörer.
Adam Edström
