About / Advertise
Det vore onekligen bra om man på något smidig sätt kunde ekvivalenstesta två kretsar redan på registernivå. Gunnar Stålmarck har lyckats med det enbart genom att addera ett stycke C-kod till konstruktionsverktygen.
- Provern lämpar sig särskilt väl i konstruktionsverktyg för ekvivalenstest av kretsar. EDA-industrin kräver hastighet och kapacitet.
Det säger Gunnar Stålmarck, grundare av och vd på programvaruföretaget Prover Technology, om sin egen uppfinning, en bevismotor för formell verifiering.
En bevismotor är en beräkningsenhet som utför komplexa logiska resonemang. Den kan exempelvis parvis nagelfara sekventiella booleska uttryck för att utröna om de uppför sig på samma sätt över tiden, oberoende av vilket tillstånd de initialt befinner sig i.
I takt med att system växer, växer också antalet möjliga kombinationer av variabelvärdena sant eller falskt. Att till exempel hitta ett baklås i en krets med hjälp av sanningstabeller blir ganska snart ogörligt.
Tidigare har konstruktionsverktygen förlitat sig på något som kallas Binary Decision Diagrams (BDD). Ett BDD är, enkelt uttryckt, en graf som kompakt representerar sanningstabellen för systemet.
- Problemet med dessa diagram är att de ofta blir väldigt stora och i värsta fall växer exponentiellt med storleken på uttrycket, säger Gunnar Stålmarck.
Bevismotorns styrka ligger i att den alltid hittar ett kort bevis när det finns ett sådant. Den är bara känslig för problemets storlek när det är nödvändigt (när det bara finns långa bevis).
Bevismetoden kan också användas i andra tillämpningar, exempelvis för DNA-analys. Det viktiga är att problemen är np-fullständiga, det vill säga kan beskrivas med logiska formler. Eftersom hårdvarubeskrivande språk som VHDL eller Verilog tämligen enkelt kan översättas i logiska uttryck, lämpar sig metoden väl för formell verifiering och modellkontroll på registernivå.
Provern består av ett stycke C-kod som säljs på licens till programvaruföretagen. Verktygskonstruktörerna skriver sina funktioner mot ett tillämpningsgränssnitt enligt ett så kallat plug-in koncept. I Stålmarcks vision ingår att bevismotorn ska bli lika vanlig i konstruktionsverktyg som till exempel stavningskontrollen i ordbehandlingsprogrammen. Företaget arbetar tillsammans med Telelogic, som ut- vecklar programvara för inbyggnad av motorn.
Stort forskarintresse
För närvarande pågår också ett samarbete med FPGA-leverantören Xilinx för nyttjande av Provern i företagets verktyg för verifiering av Virtex-familjen. Resultatet av samarbetet väntas offentliggöras i samband med att Prover i dagarna öppnar kontor i Silicon Valley. USA-kontoret har blivit möjligt genom att Intel gått in med en okänd summa pengar.
- Flera stora hård- och programvaruföretag har den här typen av forskning inom företaget, vilket är dyrt. Mycket forskning pågår på området, men vi är ganska ensamma om att ha industriella tillämpningar, säger Gunnar Stålmarck.
Med Intel i ryggen har det också blivit enklare att locka nya medarbetare. Prover består i dagsläget av 44 personer och företaget rekryterar kontinuerligt. Exakt hur många som ägnar sig åt att utveckla motorn är inte alldels lätträknat då företaget har en rad forsknings- och utvecklingsprojekt på gång.
- Många forskare tycker att det här är häftigt, säger Stålmarck, som är adjungerad professor vid institutionen för datavetenskap på Chalmers.
Industrifonden är engagerade i Prover sedan september 1999. Och fler finansiärer knackar på dörren, både svenska och amerikanska. Företaget letar dock inte efter mer kapital i dag.
Det säger Gunnar Stålmarck, grundare av och vd på programvaruföretaget Prover Technology, om sin egen uppfinning, en bevismotor för formell verifiering.
En bevismotor är en beräkningsenhet som utför komplexa logiska resonemang. Den kan exempelvis parvis nagelfara sekventiella booleska uttryck för att utröna om de uppför sig på samma sätt över tiden, oberoende av vilket tillstånd de initialt befinner sig i.
I takt med att system växer, växer också antalet möjliga kombinationer av variabelvärdena sant eller falskt. Att till exempel hitta ett baklås i en krets med hjälp av sanningstabeller blir ganska snart ogörligt.
Tidigare har konstruktionsverktygen förlitat sig på något som kallas Binary Decision Diagrams (BDD). Ett BDD är, enkelt uttryckt, en graf som kompakt representerar sanningstabellen för systemet.
- Problemet med dessa diagram är att de ofta blir väldigt stora och i värsta fall växer exponentiellt med storleken på uttrycket, säger Gunnar Stålmarck.
Bevismotorns styrka ligger i att den alltid hittar ett kort bevis när det finns ett sådant. Den är bara känslig för problemets storlek när det är nödvändigt (när det bara finns långa bevis).
Bevismetoden kan också användas i andra tillämpningar, exempelvis för DNA-analys. Det viktiga är att problemen är np-fullständiga, det vill säga kan beskrivas med logiska formler. Eftersom hårdvarubeskrivande språk som VHDL eller Verilog tämligen enkelt kan översättas i logiska uttryck, lämpar sig metoden väl för formell verifiering och modellkontroll på registernivå.
Provern består av ett stycke C-kod som säljs på licens till programvaruföretagen. Verktygskonstruktörerna skriver sina funktioner mot ett tillämpningsgränssnitt enligt ett så kallat plug-in koncept. I Stålmarcks vision ingår att bevismotorn ska bli lika vanlig i konstruktionsverktyg som till exempel stavningskontrollen i ordbehandlingsprogrammen. Företaget arbetar tillsammans med Telelogic, som ut- vecklar programvara för inbyggnad av motorn.
Stort forskarintresse
För närvarande pågår också ett samarbete med FPGA-leverantören Xilinx för nyttjande av Provern i företagets verktyg för verifiering av Virtex-familjen. Resultatet av samarbetet väntas offentliggöras i samband med att Prover i dagarna öppnar kontor i Silicon Valley. USA-kontoret har blivit möjligt genom att Intel gått in med en okänd summa pengar.
- Flera stora hård- och programvaruföretag har den här typen av forskning inom företaget, vilket är dyrt. Mycket forskning pågår på området, men vi är ganska ensamma om att ha industriella tillämpningar, säger Gunnar Stålmarck.
Med Intel i ryggen har det också blivit enklare att locka nya medarbetare. Prover består i dagsläget av 44 personer och företaget rekryterar kontinuerligt. Exakt hur många som ägnar sig åt att utveckla motorn är inte alldels lätträknat då företaget har en rad forsknings- och utvecklingsprojekt på gång.
- Många forskare tycker att det här är häftigt, säger Stålmarck, som är adjungerad professor vid institutionen för datavetenskap på Chalmers.
Industrifonden är engagerade i Prover sedan september 1999. Och fler finansiärer knackar på dörren, både svenska och amerikanska. Företaget letar dock inte efter mer kapital i dag.
Stefan Hultquist
