Moderna processorkonstruktioner ställer oss inför några av de tuffaste utmaningarna inom verifiering av hårdvara. Det gäller speciellt när det handlar om RISC-V-processorkärnor, där det finns en mängd av variationer och implementeringar från ett otal olika källor. Artikeln av W. W. Chen, N. Tusinschi och T. L. Anderson, OneSpin Solutions, presenterades på DVCon Europe 2020 och beskriver en verifieringsmetodik som finns tillgänglig för såväl leverantörer av RISC-V-kärnor som för SOC-team som arbetar med att integrera dessa kärnor. Den behandlar funktionell korrekthet inklusive komplians, upptäckt av sårbarheter i säkerheten samt verifiering av tillförlitligheten att ingen maliciös logik har lagts in. Detaljerade exempel på designbuggar som upptäckts i verkliga RISC-V-kärnor har tagits med.

Moderna processorkonstruktioner ställer oss inför några av de tuffaste utmaningarna inom verifiering av hårdvara. Sådana avancerade funktioner som flerstegs pipelines, flernivå cacheminnen, exekvering utom normal ordning, grenprediktering, spekulativ exekvering samt förhämtning är svåra att konstruera och ännu svårare att verifiera. Det finns många kombinationer av beteenden och sällsynta villkor som sannolikt inte kommer att verifieras i testbänkar som arbetar med slumpmässig simulering.

Härtill kommer att det för att ge fullt förtroende för konstruktionen krävs formell verifiering av att hårdvaran inte bara gör vad den förväntas göra, utan också att den inte gör vad den inte skall göra. Härigenom garanteras att konstruktionen är funktionellt korrekt, säker och tillförlitlig.

Verifieringen är en särskild utmaning för konstruktioner som har RISC-V-processorkärnor med många leverantörer och många varianter av implementeringen [1]. Här krävs en gemensam verifieringsmetodik som finns tillgänglig såväl för leverantörer av RISC-V-kärnor som för de SoC-team som integrerar dessa kärnor.

Figur 1. Verifieringsflöde för RISC-V

Utmaningar vid verifiering av RISC-V
RISC-V-projektet startades 2010 vid University of California i Berkeley för att definiera och implementera den femte generationens RISC-processor (Reduced Instruction Set Computer). Bland målen fanns stöd för en stor mängd olika implementeringar lämpade för olika slutapplikationer. Denna flexibilitet gav upphov till tre aspekter på RISC-V som gör dem extra svåra att verifiera.

Först har den definierade ISA:n (Instruction Set Architecture) många valbara funktioner och möjliga variationer [2, 3]. Processorn har 32 register som kan ha storleken 32-bit, 64-bit eller 128-bit. Bas-instruktionsuppsättningen (”I”) har en valbar version (”E”) som bara stöder 16 stycken 32-bits register för embedded-tillämpningar.

Bland övriga instruktioner som kan stödjas finns:
”M” – tillägg för heltals multiplikation/division
”A” – tillägg för atomisk läs-modifiera-skriv-minnesaccess
”F” – tillägg för 32-bits flyttal (single precision)
”D” – tillägg för 64-bits flyttal (double precision)
”Q” – tillägg för 128-bits flyttal (quad precision)
”C” – tillägg för komprimerade instruktioner (16-bits)

De valbara flyttalsinstruktionerna lägger till ytterligare 32 register av lämplig bredd. RISC-V:s ISA definierar tre privilegienivåer, nio exceptions associerade med privilegierade instruktioner samt 4096 styr- och statusregister (CSR). Helt klart är det en avsevärd utmaning redan att kontrollera överensstämmelsen med ISA. Men en fullständig verifiering av en RISC-V-kärna avseende funktionell korrekthet måste sträcka sig långt bortom komplians.

ISA ger möjligheter att definiera egna instruktioner, och dessa måste verifieras för att säkerställa att de arbetar korrekt utan att bryta kompliansen med standardinstruktionerna. Därtill kommer att RISC-V ISA utformades för att kunna anpassas till många olika mikroarktitekturer, från små styrkretsar till flerkärniga implementeringar med de mest avancerade processorfunktionerna.

Den som tillhandahåller kärnor måste kunna verifiera hela konstruktionen, inklusive de mikroarkitekturspecifika detaljerna, och inte bara ISA-komplians. Någon som integrerar kärnor kan tänkas vilja använda några eller alla dessa verifieringar som acceptanstest. Slutligen måste varje RTL-konstruktion (register-transfer-level) analyseras statiskt för att eliminera vanliga kodningsfel.

En metodik för RISC-V-verifiering
En metodik som uppfyller alla kraven för verifiering av RISC-V-kärnor måste baseras på formell teknologi. Alla de ansatser som baseras på simulering eller emulering kan bara utforska en liten bråkdel av funktionaliteten. Det finns inget sätt att vara säker på att konstlat slumpmässiga eller handgjorda tester hittar alla hårdvarubuggar. Det är bara formella metoder som kan ge denna garanti.

På liknande sätt kan bara formell verifiering visa om något fattas, i detta fall delar av konstruktionen som kan utgöra risker för slutapplikationer med höga krav på säkerhet och tillförlitlighet. En sådan, formellt baserad, metodik har utvecklats och använts på flera konstruktioner med RISC-V-kärnor. Denna metodik omfattar funktionell korrekthet, säkerhet och tillförlitlighet, och den kan köras av såväl leverantörer som integratörer av kärnor.

Bland indata till processen ingår kärnans RTL, de ISA-kompliansregler som samlats in formellt samt information från kärnleverantören om designdetaljer som antalet pipeline-steg, vilket möjliggör verifiering av mikroarkitekturen. Det betyder att metodiken stöder hela omfattningen av RISC-V-verifiering och klarar alla utmaningar som uppstår. Även om det ligger utanför ämnet för denna artikel kan nämnas att metodiken når ända ut till full SoC-nivå och bearbetar tillkommande verifieringsutmaningar som funktionell säkerhet och korrekt integrering av kärnan.

Funktionell korrekthet
Hjärtat i metodiken är formaliseringen av RISC-V IVA som en uppsättning av SystemVerilog Assessments (SVA) med hjälp av ett nytt Operational Assertion-bibliotek [3, 4]. Denna ansats definierar högnivåtransaktioner koncist, ungefär som i timing-diagram, och den är idealisk för att registrera de förväntade resultaten för processorinstruktioner.

Figur 2. Konceptet för Operational Assertion

Varje instruktion i RISC-V ISA fångas in i en ensam Operational Assertion som gäller för vilken som helst mikroarkitekturell implementering av instruktionen. Formella motorer verifierar att processorns tillstånd i slutet av varje instruktions exekvering överensstämmer med specifikationen.

Eftersom denna ansats är formell hittar den alla buggar som är relaterade till funktionell korrekthet och visar sedan att det inte finns några ytterligare buggar. Den är tillräckligt flexibel för att kunna hantera användarspecifika tillägg bortom ISA:n.

De formella motorerna verifierar den kompletta RISC-V-kärnan, bortom ISA-komplians, inklusive mikroarkitekturen. Metodiken uppmanar också att köra statisk analys på kärnan för att hitta allmänna designfel. Dessa sträcker sig från enkla syntaxmisstag och typografiska fel i RTL till svagheter som skulle kunna äventyra det slutliga chipet. Denna process är helt automatiserad, så många designteam ser till att den körs vid varje försök att kontrollera RTL-kod i system för revisionskontroll.

Figur 3. Operation Assertions använda på RISC-V ISA

Verifiering av säkerhet
Vissa applikationer för RISC-V-processorer har strikta säkerhetskrav så att maliciösa agenter inte kan utnyttja sårbarheter som kan finnas i konstruktionen. Säkerhetsverifiering måste innehålla en rigorös process som upptäcker alla buggar och svagheter och exakt fastslår vad som får och inte får hända i konstruktionen. I den formellt baserade verifieringsmetodiken ingår att köra ett stort antal olika automatiserade kontroller av kärnans RTL-konstruktion. Detta eliminerar snabbt många klasser av vanliga kodnings- och konstruktionsfel. Bland dessa kontroller finns:

* Strukturell analys: syntaktisk och semantisk analys av källkoden
* Säkerhetskontroller: omfattande verifiering av att det inte förekommer några vanliga designproblem med sekventiell operation
* Aktiveringskontroller: visa att alla designfunktioner kan exekveras och inte är blockerade p.g.a. oåtkomlig kod

Vissa av de problem som upptäcks av dessa kontroller utgör säkerhetsrisker som skulle kunna utnyttjas. Till exempel kan ett inkomplett case-statement sakna specifikation av vad som kommer att hända om ett oväntat värde dyker upp. Sådana problem kan hittas och åtgärdas automatiskt, tidigt i designprocessen.

Verifiering av tillförlitlighet
Oavsiktliga sårbarheter är plågsamma, men avsiktligt infogad maliciös kod (hårdvaru-Trojaner) är ett ännu större bekymmer i tillförlitlighetskritiska applikationer som autonoma fordon och kärnkraftverk. Utvecklingsprocessen för kärnor och SoC-kretsar är komplex och ger ofta många tillfällen att lägga in Trojaner.

Problem kan uppstå under logisk syntes, antingen genom avsiktliga aktiviteter eller problem med verktygen. Integration av kärnor som RISC-V-processorer ger extra risker eftersom SoC-teamen inte har detaljerad kunskap om deras uppbyggnad. Buggar i verktyg, liksom oavsiktliga modifikationer av nätlistor, kan uppstå under P&R-processen (place-and-route). Verifieringsmetodiken innehåller två steg som garanterar tillförlitligheten hos en processorkärna och som kan utöka den till att omfatta eventuellt tillagda SoC-kretsar.

Tillförlitligheten hos själva konstruktionen är beroende av hur väl formell verifiering klarar att upptäcka om en konstruktion kan göra något som den inte förväntas göra. Förutom att verifiera överensstämmelsen med RISC-V ISA kan metodiken försäkra att uppsättningen assertions täcker in hela kärnkonstruktionen. För detta krävs den nya GapFreeVerification-teknologin, som upptäcker och rapporterar eventuella brister och fel, hål i verifieringsplanen samt overifierade RTL-funktioner.

Figur 4. Flöde för GapFreeVerfication

All icke förväntad funktionalitet flaggas, för det kan vara en hårdvaru-Trojan som stoppats in under konstruktionsprocessen. De som levererar kärnor vill att deras produkter skall vara tillförlitliga, och de som använder dem vill också verifiera detta själva.

För resten av utvecklingsflödet bortom RTL-steget använder metodiken formell ekvivalenskontroll för att försäkra att ingen ny logik har lagts in under syntes- eller routningsstegen. Denna process försäkrar också att de aggressiva optimeringar som finns tillgängliga under optimeringen är lämpade för konstruktionen och inte har ändrat den på något oväntat sätt.

Genom att verifiera nätlistorna efter syntesen och routningen mot den inmatade RTL-specifikationen går det att försäkra tillförlitligheten i varje steg av utvecklingsprocessen för kärnor och SoI-kretsar.

Resultat i verkliga världen
Den beskrivna metodiken har använts på flera ställen och körts på flera olika implementeringar av RISC-V-processorer. Resultaten från två kärnor som finns tillgängliga från open-source-källor kan visas upp offentligt. Den första är RI5CY, en 32-bits implementering med en fyrstegs in-order-pipeline [6]. Den stöder instruktionsuppsättningen ”IMFC” plus kundspecifika tillägg avsedda för signalbehandling.

Figur 5. Blockdiagram över RI5CY

Verifieringsmetodiken har (när denna artikel författas) upptäckt 13 problem. Alla dessa har rapporterats tillbaka till RI5CY-utvecklarna, som har bekräftat att fyra är buggar och att tre av dem rättats. De återstående är fortfarande under utredning. Bland de problem som hittades finns:
* Inkorrekt värde skrivet till ett CSR
* Två brott mot reglerna för exception-hantering
* Sex fall där exceptions skulle ha skapats men detta skedde inte
* Inkorrekt flyttals dynamisk avrundningsmod
* Fel resultat från flyttalsberäkning
* Felaktig trap-return-hantering
* CSR:er uppdaterade under avbuggningsmod

Den andra konstruktionen som verifierats av metodiken är Rocket Core, en 64-bits implementering av RISC-V med en femstegs, ”single-issue in-order” pipelline [7]. Den har en sofistikerad mikroarkitektur med grenprediktering, instruktionsåterspelning och ”out-of-order”-avslutning för instruktioner med lång latens, som division. Fem problem hittades och rapporterades tillbaka till utvecklarna:
* Hoppinstruktioner lagrar olika ”return program counter” (PC)
* Illegala op-koder återspelas (vilket genererar minnesaccesser)
* DIV-resultat (division) inte skrivna till registerfil
* Resultat från avbuggningsläget kan exekveras utanför detta läge
* Kärnan innehåller odokumenterade, icke-standardiserade instruktioner

Figur 6. Blockdiagram över Rock Core

Det första problemet betraktades inte som en bugg eftersom enheten som hämtar instruktioner har ansvaret att förhindra att detta händer. Det andra är fortfarande under utredning. De återstående tre problemen har bekräftats vara buggar och har korrigerats av utvecklarna.

Den sista buggen är särskilt intressant. De formella motorerna rapporterade att kärnan innehöll en icke förväntad instruktion som mycket väl hade kunna vara en hårdvaru-Trojan. Det visade sig att utvecklingsteamet hade lagt till en ny instruktion. Men de hade ännu inte dokumenterat den i den specifikation som teamet använder för att utveckla Operational Assertions för egna instruktioner. Så integrationsteam som laddat ner samma version av kärnan skulle ha okänd och odokumenterad funktionalitet i konstruktionen, och bara GapFreeVerification skulle ha upptäckt och rapporterat detta.

Verktyg
Verifieringen av de båda kärnorna utfördes med hjälp av en metodik och verktyg som tillhandahållits av OneSpin Solutions. Här ingår den formella plattformen DV-Verify, Floating-Point Unit App, RISC-V Verification App samt EC-ASIC och EC-FPGA för ekvivalenskontroll [8].

Slutsats
RISC-V håller på att omvandla processor- och SoS-industrin, men ger också utmaningar vid verifieringen för både leverantörer och SoC-integratörer. Verifiering måste sträcka sig långt bortom ISA-komplians för att täcka in mikroarkitekturer, kundanpassningar, säkerhet och tillförlitlighet.

Denna artikel beskriver en metodik som omfattar hela detta område. Dess värde har bevisats med resultaten från verifiering av två populära open-source RISC-V-kärnor. Båda har verifierats och tejpats ut flera gånger, men ändå har metodiken funnit kvarvarande designbuggar som verifierats av kärnutvecklarna. Utvecklare och integratörer av kärnor behöver inte längre hitta buggar i kisel. En tredjepartslösning, som kan användas av båda parter och som gör det möjligt att ta fram RISC-V-konstruktioner som uppfyller de högsta kraven på funktionalitet, säkerhet och tillförlitlighet, finns tillgänglig idag.

W. W. Chen, OneSpin Solutions, München
N. Tusinschi, OneSpin Solutions, München
T. L. Anderson, OneSpin Solutions, San Jose
Artikeln presenterades på DVCon Europe 2020.

REFERENSER

[1] www.risc-v.org.
[2] The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20190608-Base-Ratified.
[3] The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, Document Version 20190608-Priv-MSU-Ratified.
[4] R. Baranowski and M. Trunzer, ”Complete formal verification of a family of automotive DSPs”, DVCon Europe, 2016.
[5] J. Bormann, S. Beyer, A. Maggiore, M. Siegel, S. Skalberg, T. Blackmore, and F. Bruno, ”Complete formal verification of TriCore2 and other processors”, DVCon, 2007.
[6] github.com/pulp-platform/riscv
[7] github.com/chipsalliance/rocket-chip
[8] www.onespin.com/products/360-dv-verify/

Filed under: Fordonselektronik