Man kan helt säkert säga att intresset för RISC-V uppvisar en kraftig ökning inom konstruktörskretsar. Det handlar inte bara om att hela idén bakom open-source gjort det till ett kostnadseffektivt alternativ, utan också om att dess ISA (instruction set architecture) är uppbyggd för att ge stor flexibilitet. Rob van Blommestein, Vice President of Marketing, OpenSpin Solutions, tittar här på vad det innebär för verifieringen av RISC-V.

Instruktionssetet hos RISC-V kan mappas till många olika implementeringar och mikroarkitekturer, har ett stort antal valbara instruktioner och funktioner samt stöder ett brett register av slutapplikationer. Men denna flexibilitet leder också till problem vid verifieringen, liksom frågor om hur man på bästa sätt skall lösa dessa problem.

Det finns ett antal krav som måste uppfyllas när man utvecklar och använder RISC-V-kärnor. Ett av de viktigaste är att det går att ha förtroende för IP-implementeringen. Har alla funktioner implementerats? Har de implementerats korrekt? Finns det några buggar som gömt sig i implementeringen? Finns det några dolda Trojaner? Med simulering har det dock varit svårt att få svar på dessa frågor, vilket medfört en ökad användning av formell verifiering för att besvara dem. Den djupgående naturen hos formell verifiering gör att detta är det idealiska valet för att kunna försäkra sig om att få förtroende för kärnan.

För att kunna ge en djupare förståelse för hur man effektivt kan verifiera RISC-V frågade vi konstruktörskretsen om man hade några specifika frågor angående detta. Nedan finns ett antal sådana frågor, med tillhörande svar av våra egna experter på OneSpin.

F: Finns det någon speciell formell metodik enbart för RISC-V?

S: Det finns inte något specifikt för RISC-V. Men man måste ha en ganska ingående förståelse för RISC-V:s ISA för att kunna skapa den korrekta uppsättningen egenskaper (properties) och garantera att denna uppsättning är komplett.

En formell teknik som bör användas för att skapa egenskaperna är ”interval properties checking”. Detta är återanvändbara SystemVerilog Assertions som används för att få fram en obegränsad bevisning. Det finns flera viktiga aspekter på dessa Assertions. De startar inte från reset utan från ett generiskt giltigt tillstånd. Det finns bara ett begränsat antal cykler tillgängliga för att uppnå detta generiskt giltiga tillstånd. Det är viktigt att man frikopplar ISA-specifikationskraven från de mikro-arkitektoniska detaljerna.

Interval Property Checking

Dessa operativa SystemVerilog Assertions gör det möjligt att ta fram icke överlappande Assertions på högnivå som fångar upp slut-till-slut-transaktioner och krav på ett koncist och elegant sätt:

* Fånga upp funktionella krav i ett formellt och för simulation exekverbart format
* Fånga upp kompletta kretstransaktioner på ett koncist och elegant sätt, liknande timing-diagram
* Uppnå 100 % funktionell täckningsgrad med Assertions på högnivå som är enkla att granska
* Införa en konsekvent Assertion-style som kan sättas in för ett stort antal olika applikationer, och som kan ge optimala prestanda för både simulatorer och formella verktyg
* Tydligt separera implementeringsspecifik, stödjande verifieringskod från återanvändbar kod på specifikationsnivå

Man behöver konstruera ett stort antal egenskaper för att fullt ut kunna verifiera RISC-V-konstruktionen. Detta kan komma att ta flera månader att genomföra och kräver detaljerad kunskap om det formella verktyget för att uppnå fullständig täckning. Det finns lösningar på markanden som drastiskt kan förkorta denna tid.

F: RISC-V är en mycket omfattande konstruktion, så hur kan den verifieras och vilka initiala antaganden krävs?

S: Det är svårt att svara på vilka de initiala antagandena skall vara eftersom dessa är olika beroende på den specifika konstruktionen.

Men när man tar sig an att verifiera en enorm konstruktion som en RISC-V-kärna är den bästa metoden att dela upp och besegra. Att fokusera på kärnan skall vara det första steget. Här ingår att se till att inget bryter mot protokollen, verifiera cacherna separat för att upptäcka tillhörande komplexiteter, se närmare på sammankopplingarna mellan olika block samt utföra ”x-propagation”. Det är viktigt att notera att x-propagation skall utföras på block- och enhetsnivå och inte på hela kärnan under detta steg. En annan metod är att använda ”assume guarantee” för att validera gränssnitten.

Det är värt att nämna att dessa metoder inte är specifika för RISC-V, utan de kan användas vid alla former av processorverifiering. Men eftersom RISC-V är så komplicerat kan det krävas flera månader för att utföra en komplett och djupgående verifiering a kärnan.

Det finns lösningar på marknaden, som OneSpins Processor Verification, som har konstruerats med dessa komplexiteter i åtanke för att generera återanvändbara assertion-IP och genomföra en fullständig verifiering på en bråkdel av tiden.

F: Vilka fördelar uppnår man genom att använda formell verifiering istället för simulering på ett företag som vill certifiera en RISC-V-implementering mot säkerhetskritiska standarder?

S: En av de viktigaste fördelarna som formell verifiering ger jämfört med simulering är den grad av djupgående grundlighet som kan uppnås. Detta gäller inte bara för RISC-V, utan för alla processorer. Det viktigaste är att vid ökande komplexitet når man en punkt där simulering inte längre är tillräckligt. För dagens konstruktioner ligger denna komplexitetströskel ganska lågt. Vad gäller RISC-V går det att utföra en djupgående verifiering om man har korrekta kunskaper om ISA, den kompletta uppsättningen egenskaper samt de rätta formella motorerna.

Formell verifiering ger mycket kraftfullare resultat än att bara köra en traditionell komplians-testsvit i en simulering. Simulering, oavsett hur omfattande den är, kan bara testa en ytterst liten bråkdel av alla möjliga uppträdanden hos konstruktionen. Till och med de mest omsorgsfullt framtagna komplians-testsviterna lämnar stora gap i täckningsgraden.

Det finns otaliga exempel där specifika operandvärden eller perifert uppstående villkor lämnas otestade, och några av dessa kan trigga dolda designbuggar. Detta gäller i extra hög grad för aritmetiska operationer. Ett enda felskrivet arrayindex i en RTL-beskrivning kan ge en konstruktion där oväntade och icke intuitiva operander ger felaktiga svar. Själva naturen hos simulering, liksom hos acceleration och emulering, gör det omöjligt att testa varje möjligt fall. Formella verktyg itererar sig inte genom testfall, utan de analyserar matematiskt konstruktionen i sin helhet.

När det handlar om säkerhet är det mycket viktigt att veta om det går att undvika sårbarheter, hur och var alla eventuella buggar finns samt om alla vägar är korrekta. Med simulering är det svårt att få en komplett bild. Det finns en gräns för hur långt det lönar sig att gå när fortsatta körningar misslyckas med att hitta alla svar. Formell verifiering är den enda teknologin som slutgiltigt kan bevisa avsaknaden av något (t.ex. buggar). Det finns säkerhetsstandarder som kräver att man använder specifika verifieringsmetoder, liksom en väldefinierad och djupgående verifieringsprocess. Det betyder att verifieringen måste vara mycket mer rigorös. Om säkerhet är en viktig faktor är enbart simulering inte tillräckligt, utan formell verifiering måste vara en del av verifieringsplanen.

F: Jag har hört att RISC-V-kärnan är skriven i Chisel. Hur klarar formell verifiering detta?

S: Det finns ett fåtal open-source-kärnor, som de från Berkeley, som är skrivna i Chisel. Men de flesta formella lösningar stöder inte direkt detta språk. Det finns många metoder som enkelt kan översätta Chisel till Verilog och som har brett stöd av formella verktyg på marknaden. Det finns naturligtvis också många RISC-V-kärnor som är skrivna direkt i Verilog, så här uppstår inga sådana problem.

F: Måste jag verifiera att en RISC-V-kärna som jag får från en leverantör är buggfri?

S: Kort sagt är svaret ja. Leverantören bör köra en komplett verifiering av integriteten hos kärnan och tillhandahålla dokumentation av resultaten. För att ge förtroende för integriteten hos kärnan bör formell verifiering vara en del av deras verifieringsflöde.

Bara det faktum att kärnan har verifierats formellt betyder dock inte att integrationen av den in i konstruktionen kommer att vara ren och problemfri. Alla verifieringssteg bör köras igen när RISC-V-kärnan läggs in i den slutliga konstruktionen.

F: Hur verifierar jag att en RISC-V-kärna har integrerats korrekt in i en konstruktion?

S: En rekommendation är att använda en formell lösning anpassad efter komplexiteten hos RISC-V. I processen måste ingå automatiserad inspektion av koden för att snabbt kunna eliminera många klasser vanliga kodnings- och designfel innan den formella verifieringen och logiska syntesen påbörjas. Verifieringen av RTL bör utföras utifrån tre olika perspektiv:

* Strukturell analys: fokuserad syntaktisk och semantisk analys av källkoden
* Säkerhetskontroller: djupgående verifiering av att det inte förekommer några allmänna operationsproblem med den sekventiella konstruktionen
* Aktiveringskontroller: visa att specifika designfunktioner kan exekveras och inte är blockerade på grund av icke åtkomlig kod

Kontroll av intervallegenskaper bör också användas, som beskrivs ovan i svaret på frågan ”Finns det någon speciell formell metodik enbart för RISC-V?”

F: Jag har lagt till en egen instruktion. Behöver jag verifiera hela RISC-V-kärnan igen?

S: Så snart något gjorts för att modifiera en instruktion betyder det att funktionalitet har lagts till eller ändrats. För att vara säker på att konstruktionen fungerar som avsetts och inte gör något icke önskat är det rekommendabelt att utföra en ny, fullständig verifiering.

F: Jag behöver en buggfri RISC-V-kärna. Vilken leverantör eller open-source-källa bör jag använda?

S: Sök efter en leverantör som tillhandahåller open-source-kärnor som har blivit ytterst grundligt verifierade med formella metoder. Detta minskar drastiskt riskerna för att buggar letar sig in i den slutliga konstruktionen. Glöm inte att efterfråga dokumentation om leverantörens verifieringsprocess så att du kan vara säker på att formell verifiering har använts. En bra plats att utgå från för att hitta formellt verifierade open-source-kärnor är OpenHW Group (www.openhwgroup.org).

Som vi sett ger RISC-V fördelarna av flexibilitet och anpassningsbarhet, förutom att det sänker processorernas kostnadsbarriär. Men med dessa fördelar följer en ökad komplexitet som kan komplicera verifieringsprocessen. Att förstå vilka verifieringsproblem som kan uppstå och hur man löser dessa är en nödvändighet för varje konstruktör som är intresserad av RISC-V. Vi hoppas att de svar vi givit har ökat förståelsen för hur verifiering och tillhörande verktyg och metoder skall användas för att åstadkomma en komplett verifiering.

Rob van Blommestein, Vice President of Marketing, OpenSpin Solutions

Filed under: EDA, Mikroprocessorer