Två trappor upp vid Mariatorget i Stockholm ligger Logikkonsult NP, Europas - förmodligen - äldsta och största företag inom formella metoder.

Företaget vill nu nå en bredare publik och söker därför en partner. Gärna stor, rik och amerikansk.

- Vi vet att vårt verktyg fungerar. Nu vill vi nå ut på den breda marknaden och måste därför liera oss med ett större företag.

Orden kommer från Arne Borälv som i snart tre år blandat utvecklingsarbete med konsultuppdrag på Logikkonsult NP AB. Det både syns och hörs att han tror på sitt skötebarn, det formella verifieringsverktyget Prover.

- Prover är mycket mognare än andra verifieringsverktyg på marknaden. Det har utvecklats under lång tid och kommit en generation längre.

Och visst har verktyget en diger meritlista - Prover används av tiotalet kunder i Europa, främst i Sverige. Det har verifierat krav i Saabs JAS-plan, hittat fel i styrsystemet för Madrids tunnelbana och i specifikationen för Volvos bussar. Hittills har det främst rört verifiering av specifikationer och system, men verktyget klarar även att analysera hårdvara såväl som tillämpningsprogram.

Arne Borälv, som är produktchef för Prover, vill nu fokusera hårdare på just hårdvaruverifiering, ett område där formella metoder tros få allt större betydelse.

- Vi har använt Prover för att verifiera VHDL-kod och det står sig mycket bra jämfört med konkurrerande verktyg, säger han stolt.



Svårt för liten svensk


Men ett litet svenskt företag har inte lätt att slå sig in på den USA-dominerade verktygsmarknaden. En stor amerikansk firma i ryggen är ofta enda chansen att nå internationell framgång. Syntesföretaget Synthesia och modellföretaget Axiom är två svenska företag som numera går under amerikansk flagg, efter att ha blivit uppköpta av Cadence respektive Mentor Graphics.

Men så långt som till att bli uppköpt vill Arne Borälv inte gå. Han siktar istället på en allians med en verktygsleverantör som då kan licensiera Prover och integrera det i sin egen produktportfölj. Vidareutvecklingen av verktyget vill han att Logikkonsult NP skall sköta på Södermalm i Stockholm även i fortsättningen.

- Vi samtalar nu med en av de fyra största verktygsleverantörerna plus ett mindre företag i genren, säger Arne Borälv.

"En av det fyra största" betyder Cadence, Synopsys, Mentor eller Viewlogic. En av de mindre kan vara Abstract Hardware eller Chrysalis, två företag som specialiserat sig på just formell verifiering av hårdvara. Vilka det rör sig om vill han inte avslöja, förhandlingarna är långt ifrån färdiga.



Hokus pokus


För den oinvigde kan själva tekniken låta lite hokus pokus. Man formulerar frågor av typen "Kan två mötande tåg få grönt ljus samtidigt?" eller "Kan skrivsignalen till en minnessektor vara aktiv samtidigt som lässignalen?". Verktyget ger sedan snabbt besked. Mycket snabbt till och med.

Arne Borälv demonstrerar exemplet från Madrids tunnelbana och med 36 000 variabler tar körningen en halv minut. Och då tog det endast en dag att förbereda körningen.

- Det svåra är egentligen att ställa rätt frågor. En bra kravspec underlättar oerhört, säger Arne Borälv.

Hans företag ger därför även kurser i konsten att skriva heltäckande, konsistenta kravspecifikationer.

Kan man verifiera vilken typ av konstruktion som helst med ert verktyg?

- Nej realtidstillämpningar är svårare. Annars fungerar verktyget bra för system som skapats av människor. De har så låg svårighetsgrad, säger Arne Borälv.

När jag ber om exempel så börjar han snabbt rabbla tillämpningar som knappast brukar kallas simpla, som delsystem till JAS och kärnkraftverk plus tjänsteinteraktion inom telefoni. Men Arne Borälv förtydligar:

- Svårighetsgraden beror på hur många antaganden man måste göra i beviset. Och människoskapade system bygger på relativt få sådana antaganden.

Charlotta von Schultz



Mer filosofi än elektronik


Formella verktyg bygger på matematiska metoder. Allt känns inte solklart för den som har hårdvarubakgrund. Men som Arne Borälv, datavetare från Uppsala, uttrycker det:

- Det här föddes inte i hårdvaruvärlden. Det föddes inom filosofin.

Logikkonsult NPs produkter - Prover och NP-Tools - baseras på den mångfaldigt patenterade Stålmarcksmetoden, som beskrivs som "ett naturligt deduktivt bevissystem med ett unikt angreppssätt på begreppet bevisdjup". Ett bevis- djup definieras som det största antalet nästlade antaganden i beviset.

Bevismetoden klarade först enbart boolesk algebra men hanterar numera även heltalsaritmetik.

Gunnar Stålmarck, som idag sitter i VD-stolen, var en av grundarna när företaget startades 1989.

CvS