Formell verifiering är en av de många teknologier som lovat att revolutionera konstruktörernas arbete och som inte riktigt klarat att nå hela vägen fram. Men med en lite mera ”avslappnad” affärsmodell ser det nu ut att gå betydligt bättre. Samma sak gäller förresten sådant som konfigurerbara processorer och kiselkompilering.

Det är inte alltid lätt att ha en fantastisk lösning och ändå misslyckas med att erövra världen. Inom halvledarvärlden är det mer uppenbart än på många andra ställen. Forskningsvärlden genererar revolutionerande idéer, företag startas för att kommersialisera det hela och användarna vägrar ändå att lämna sina invanda metoder.

I efterhand visar det sig förstås ofta att användarna hade rätt. De nya, fantastiska metoderna var bra ”i princip”, men dög inte riktigt som genomgripande lösning. Det blev lite för många stora löften, med lite för många ”hål” i arbetsflödet.

Formell verifiering
Inom EDA-världen, alltså de företag som tillverkar konstruktionsverktyg för halvledarkonstruktion, är kanske formell verifiering det senaste stora försöket att förändra arbetet i grunden. Det innebär i och för sig inte att formell verifiering är något nytt. Inom forskningsvärlden har principerna diskuterats sedan mitten av nittonhundratalet och formella metoder för verifiering av mjukvara har använts åtminstone sedan sjuttio- och åttiotalet.

Men de stora satsningarna inom EDA-världen kom först runt millenieskiftet. Då fanns det gott om nystartade företag som ville kommersialisera formell verifiering i alla sina skepnader. Helst skulle formell verifiering bli huvudspåret inom verifiering.

Så blev det nu inte. Alla de stora halvledarföretagen använde simulering som grundläggande verifieringsmetod och ytterst få var intresserade av att skifta tankesätt. Så det var bara att anpassa sig och lansera formell verifiering som dellösning i stället för huvudspår. Det fungerade ganska bra, inte minst i Japan.

Idag har de flesta av de här företagen köpts upp av de tre stora: Cadence, Synopsys och Mentor. Där ligger formell verifiering som en del i en större verifieringslösning. Ofta handlar det om att kunna verifiera färdiga IP-block på ett smidigare sätt.

Appar
Den modell för formell verifiering som nu lanseras av OneSpin Solutions är ovanligt intressant. Man överlåter helt enkelt mycket av arbetet på tredjepartsföretag som ligger närmare slutkunden. Det kan handla om verifiering av standarder eller lite vad som helst. Tredjepartsföretaget använder OneSpins verktyg och ”motorer” vid utvecklingen och kan sedan låta hela eller delar av verktygssviten hänga med sin produkt. Slutkunden ser inte verktygen från OneSpin, utan bara ”högnivåverktyget” från tredjepartsleverantören.

På det här sättet blir det möjligt för en slutanvändare att använda en teknologi utan att tvingas betala hela kostnaden eller tvingas lära sig allt. Det är viktigt, eftersom den här typen av verktyg både är dyra och har en hög inlärningströskel.

Konfigurerbara processorer
Backar vi ytterligare några år blir modeordet konfigurerbara processorer. Också här kommer tekniken från forskarvärlden och målet för de mest långtgående projekten var att automatiskt kunna generera optimerade processorer och utvecklingsmiljöer utifrån en viss programvara.

I praktiken var det inte lika lätt att konkurrera med generella processorer. En automatgenererad konstruktion kanske i princip är effektivare, men handoptimerade generella processorer blir ändå tillräckligt bra, billigare och framför allt säkrare för slutanvändaren. Redan att kunna välja mellan flera tillverkare av utvecklingsverktyg har ett stort värde.

Däremot finns det en hel del specialtillämpningar där en specialprocessor kan snabba upp exekveringen. Det kan till exempel handla om audiotillämpningar eller videotillämpningar där extrem optimering kan ge dramatiskt högre prestanda eller lägre energiförbrukning.

I dag verkar tillverkarna av konfigurerbara processorer ha hittat sina nischer. De fornstora tankarna är borta och i stället har man begränsat sig till de områden där tekniken är konkurrenskraftig. Och sådana finns.

Kiselkompilering
Och om vi backar tillbaka hela vägen till åttiotalet (och nittiotalet) stöter vi ofta på ordet kiselkompilering. Flera av de stora halvledartillverkarna satsade hårt på den tekniken.

En av finesserna med kiselkompilering var och är att tekniken går hela vägen till kisel. En högnivåbeskrivning genererar en, ofta mycket vacker, kiselstruktur, där det är lätt att se de olika funktionsblocken och gränssnitten.

Nu är ju skönhet och elegans inte särskilt mycket värt i halvledarsammanhang. De betydligt fulare chip som blir resultatet med först logiksyntes och sedan ”vanlig layout” har en ovana att vara mindre och billigare. Gissa vilken teknik som vann.

Men kiselkompilatorn finns ändå kvar i en begränsad form. När man till exempel vill göra ett minnesblock kommer tekniken till si rätt. Men inte blev det som många hade tänkt sig.

Det är lätt att gapa över för mycket.

Filed under: Göte Fagerfjäll