About / Advertise
Matematiska, formella verktyg som snabbt och uttömmande hittar felen i en konstruktion håller på att få fotfäste bland konstruktörer. Tekniken är mogen för genombrott, men än är det svårt att identifiera vilket angreppssätt som är bäst och vilken leverantör som blir marknadsledande.
- Verktyg för formella metoder kan förändra hela konstruktionsarbetet. Det kan blir lika viktigt för konstruktionsbranschen som när syntesverktygen kom för tio år sedan, säger Rick Carlson, marknadschef på företaget Averant.
Det skulle kunna vara avancerat säljsnack, men att döma av den stora mängd verktyg som lanserades på Date så är han långt ifrån ensam i sin tro. Mässan formligen kryllade av produkter och ambitioner inom ämnet formell verifiering. Många kom från små och måttligt kända företag, som Averant, Real Intent, Valiosys, Verisity och Esterel. Andra företag har några år på nacken, som Transeda och för stunden marknadsledande Verplex. Flera av företagen har styrelsemedlemmar eller rådgivare hämtade bland branschens veteraner.
De stora i branschen är givetvis medvetna om läget. Mentor Graphics, till exempel, har en särskild avdelning för ämnet och lanserade förra året sitt första verktyg för ändamålet, må vara på en rätt fundamental nivå.
Att intresset är så stort hänger förstås samman med industrins enorma behov av att korta ned tiden för verifieringsarbetet. Idag tar verifiering i genomsnitt mellan 50 och 55 procent av konstruktionstiden - men skräckexempel på 80-90 procent nämns också. Problemet blir ju dessutom allt värre i takt med att konstruktionerna ökar i storlek och komplexitet. Simulering förslår helt enkelt inte längre.
Hittar varje fel
Det som tilltalar konstruktörerna inte bara hoppet om snabbare verifieringsarbete, utan också löftena om radikalt ökad kvalitet. åtminstone i teorin går det att hitta bokstavligt talat varenda fel, något som man aldrig kan vara säker på hur mycket simuleringar som än görs.
Alla verktyg för formell verifiering gör förvisso inte samma sak. De mest avancerade, som rönte störst intresse på Date, försöker sig på att höja abstraktionsnivån ovanför registernivån, och använder formella metoder för att se om konstruktörens verkliga avsikter avspeglas i konstruktionen, samt att denna är funktionellt korrekt.
Området är så nytt att det inte har fått något etablerat samlingsnamn ännu, men funktionell kontroll (functional checker) och avsiktsstyrd verifiering (intent-driven verification) är några benämningar som används.
Kräver egna språk
Många av dessa verktyg kräver ett eget konstruktionsspråk, mer eller mindre närbesläktat med C, C++, VHDL eller Verilog. Andra utnyttjar möjligheterna att sätta in kommentarer i VHDL- eller Verilogkoden, och låter verktyget styras av dessa kommentarer. Om detta är en utvidgning av dessa språk eller bara ett smart sätt att utnyttja dess möjligheter kan man diskutera.
Funktionell kontroll kan ses som en utvidgning av modellkontroll (model checking) som hittills ansetts som det mest avancerade. Skillnaden är något hårdraget att funktionell kontroll kräver ett mer formaliserat sätt att beskriva avsikt och beteende, men ger i gengäld en nära hundraprocentig feltäckning och en metodik för att åtgärda felen.
Oavsett benämning är detta väsensskilt från ekvivalenskontroll, den enklaste typen av formell verifiering. Där jämförs enbart en beskrivning på registernivå (RTL, register transfer level) med en annan på grindnivå, alternativt två olika beskrivningar på grindnivå, och svarar på frågan om dessa beskriver samma funktion. Däremot finns ingen kontroll på att beskrivningen på registernivå har avsedd funktion, eller att den följer specifikationen.
Användarvänlighet i fokus
Pessimisterna pekar på att teorierna för formell verifiering varit allmänt kända i den akademiska världen i tiotals år, men att de visat sig vara svåra att använda i praktiken. Men detta stämmer inte längre. Användarvänlighet är numera en ledstjärna för de flesta verktygstillverkare, och branschen är synnerligen försiktig med att lansera nymodigheter som stör etablerade konstruktionsmetoder och -flöden.
Ingen tror i dagsläget att formella metoder helt kommer att ersätta simulering. Därtill är verktygen alltför outvecklade. Men den uppsjö av nya företag och intressanta verktyg som kommit fram på detta område indikerar att formella metoder kommer att bli en viktig pusselbit i många konstruktionsflöden framöver. Vilken leverantör som sedan kommer att dominera återstår att se.
Tiden som går åt till simulering ökar exponentiellt med summan av antalet ingångar och tillstånd. En uttömmande simulering kräver så många vektorer som 2 upphöjt till denna summa. även med en snabb simulator som klarar en miljon vektorer per sekund, så blir simuleringstiderna lätt ohållbara. I teorin kräver ett stort system på kisel simuleringstid motsvarande hela jordens eller rentav universums historia!
Det skulle kunna vara avancerat säljsnack, men att döma av den stora mängd verktyg som lanserades på Date så är han långt ifrån ensam i sin tro. Mässan formligen kryllade av produkter och ambitioner inom ämnet formell verifiering. Många kom från små och måttligt kända företag, som Averant, Real Intent, Valiosys, Verisity och Esterel. Andra företag har några år på nacken, som Transeda och för stunden marknadsledande Verplex. Flera av företagen har styrelsemedlemmar eller rådgivare hämtade bland branschens veteraner.
De stora i branschen är givetvis medvetna om läget. Mentor Graphics, till exempel, har en särskild avdelning för ämnet och lanserade förra året sitt första verktyg för ändamålet, må vara på en rätt fundamental nivå.
Att intresset är så stort hänger förstås samman med industrins enorma behov av att korta ned tiden för verifieringsarbetet. Idag tar verifiering i genomsnitt mellan 50 och 55 procent av konstruktionstiden - men skräckexempel på 80-90 procent nämns också. Problemet blir ju dessutom allt värre i takt med att konstruktionerna ökar i storlek och komplexitet. Simulering förslår helt enkelt inte längre.
Hittar varje fel
Det som tilltalar konstruktörerna inte bara hoppet om snabbare verifieringsarbete, utan också löftena om radikalt ökad kvalitet. åtminstone i teorin går det att hitta bokstavligt talat varenda fel, något som man aldrig kan vara säker på hur mycket simuleringar som än görs.
Alla verktyg för formell verifiering gör förvisso inte samma sak. De mest avancerade, som rönte störst intresse på Date, försöker sig på att höja abstraktionsnivån ovanför registernivån, och använder formella metoder för att se om konstruktörens verkliga avsikter avspeglas i konstruktionen, samt att denna är funktionellt korrekt.
Området är så nytt att det inte har fått något etablerat samlingsnamn ännu, men funktionell kontroll (functional checker) och avsiktsstyrd verifiering (intent-driven verification) är några benämningar som används.
Kräver egna språk
Många av dessa verktyg kräver ett eget konstruktionsspråk, mer eller mindre närbesläktat med C, C++, VHDL eller Verilog. Andra utnyttjar möjligheterna att sätta in kommentarer i VHDL- eller Verilogkoden, och låter verktyget styras av dessa kommentarer. Om detta är en utvidgning av dessa språk eller bara ett smart sätt att utnyttja dess möjligheter kan man diskutera.
Funktionell kontroll kan ses som en utvidgning av modellkontroll (model checking) som hittills ansetts som det mest avancerade. Skillnaden är något hårdraget att funktionell kontroll kräver ett mer formaliserat sätt att beskriva avsikt och beteende, men ger i gengäld en nära hundraprocentig feltäckning och en metodik för att åtgärda felen.
Oavsett benämning är detta väsensskilt från ekvivalenskontroll, den enklaste typen av formell verifiering. Där jämförs enbart en beskrivning på registernivå (RTL, register transfer level) med en annan på grindnivå, alternativt två olika beskrivningar på grindnivå, och svarar på frågan om dessa beskriver samma funktion. Däremot finns ingen kontroll på att beskrivningen på registernivå har avsedd funktion, eller att den följer specifikationen.
Användarvänlighet i fokus
Pessimisterna pekar på att teorierna för formell verifiering varit allmänt kända i den akademiska världen i tiotals år, men att de visat sig vara svåra att använda i praktiken. Men detta stämmer inte längre. Användarvänlighet är numera en ledstjärna för de flesta verktygstillverkare, och branschen är synnerligen försiktig med att lansera nymodigheter som stör etablerade konstruktionsmetoder och -flöden.
Ingen tror i dagsläget att formella metoder helt kommer att ersätta simulering. Därtill är verktygen alltför outvecklade. Men den uppsjö av nya företag och intressanta verktyg som kommit fram på detta område indikerar att formella metoder kommer att bli en viktig pusselbit i många konstruktionsflöden framöver. Vilken leverantör som sedan kommer att dominera återstår att se.
Tiden som går åt till simulering ökar exponentiellt med summan av antalet ingångar och tillstånd. En uttömmande simulering kräver så många vektorer som 2 upphöjt till denna summa. även med en snabb simulator som klarar en miljon vektorer per sekund, så blir simuleringstiderna lätt ohållbara. I teorin kräver ett stort system på kisel simuleringstid motsvarande hela jordens eller rentav universums historia!
Adam Edström
