Coding Styles för SystemC/C++ har visserligen använts i många år, men det är först på senare tid som specifika användningsmodeller har tagits fram för att driva på gemensamma designflöden bland konstruktionsteamen. Bland dessa finns att använda abstrakt algoritmisk designkod som indata till HLS-verktyg (High Level Synthesis), virtuella plattformsmodeller för tidig mjukvarutest, konfigurerbara IP-block och därtill många fler. Vlada Kalinic, produktchef för SystemC Formal Verification på OneSpin, ett Siemens-företag beskriver här hur formell verifiering kan effektivisera konstruktionsarbetet. Artikeln presenterades ursprungligen vid DVCon Europe 2021.

HLS, som omvandlar ”mestadels icke tidsmärkta”, abstrakta designrepresentationer i SystemC/C++ till fullt tidsmärkta RTL-designblock, används av många stora halvledar- och systemleverantörer. HLS-verktyg är speciellt populära att använda som en metod att snabbt generera designkomponenter med olika mikroarkitekturer, samtidigt som de optimerar datavägar för algoritmbearbetning snabbt och effektivt. De får därför en allt större användning i styrlogik, och som komponenter med generellt mer detaljerad timing.

Verifiering av konstruktioner i SystemC/C++ utförs huvudsakligen genom att man kompilerar designrepresentationen med hjälp av en vanlig mjukvarukompilator, t.ex. GNU Compiler Collection (GCC), och avbuggar koden ungefär som en mjukvarukonstruktion. Med Open SystemC International (OSCI) SystemC/C++ Class Library, som nu har standardiseras som IEEE 1666-2011, kom möjligheter som ger användarna en mer RTL-simuleringsliknande upplevelse. Men det kvarstår fortfarande många problem som gör verifieringen av SystemC-kod till en komplex och mödosam uppgift, som avbuggning, körprestanda och testkomplexitet. Tillgången till formella metoder på denna nivå har varit sparsamma.

Ett vanligt HLS-flöde för SystemC/C++ använder algoritmiska beskrivningar som ofta bara använder C- eller C++-kod. Dessa beskrivningar testas för att garantera att själva algoritmen fungerar korrekt. Biblioteksfunktionerna av SystemC-klass används för att ge minimal detaljeringsgrad av hårdvaran, som grundläggande timing och reset-funktionalitet, när HLS-verktygen kräver det. Syntesverktygen producerar RTL-kod, som sedan används i mer traditionella processer för förfining av konstruktionen samt verifiering.

Verifieringen av konstruktionen delas upp mellan SystemC- och RTL-nivåer. Ingenjörerna skulle föredra att avbugga och verifiera de ursprungliga SystemC-konstruktionerna, och bara kontrollera en funktionell ekvivalens efter syntesen, ungefär som i traditionella RTL-utvecklingsprocesser. Men avsaknaden av effektiva miljöer för designverifiering av SystemC/C++ har styrt över ingenjörerna till traditionell HDL-verifiering.

I takt med att ingenjörerna höjt abstraktionsnivån på sina designansatser har det blivit alltmer naturligt att också höja nivån på verifieringen. På den algoritmiska nivån före HLS är det ett krav att man verifierar konstruktionen direkt mot dess specifikation utan att alltför mycket se på detaljer i kodningen. Funktionella specifikationer kan enkelt representeras med ”assertions”. Formella tekniker, som gör det möjligt att rigoröst testa assertions mot konstruktionen, blir det naturliga valet. Nya kontrollintensiva algoritmer, som nu kodas i SystemC, är extra svåra att verifiera enbart med hjälp av simulering.

Vi har utvecklat en assertions-baserad formell metodik som gör det möjligt att använda ett brett register av formella tekniker för att konstruera komponenter som kodats i C++ eller SystemC, med olika nivåer på timing och kodabstraktion.

Vi föreslår att man använder en uppsättning av automatiserade (som en tryckknappslösning) struktur-, säkerhets- och aktiveringskontroller som kan användas på konstruktioner utan att man manuellt behöver skapa några assertions. Detta är speciellt användbart för sign-off av designkod före högnivåsyntes.

Vi föreslår också att man använder formella tekniker på designkod i SystemC/C++ för att eliminera buggar tidigare i designprocessen. Många problem kan slinka genom vid simulering eller högnivåsyntes. Det kan gälla oavsiktligt beteende orsakat av problem med specifika datatyper, t.ex. flyttalsaritmetik, eller tidsrelaterade problem som utvärdering av ”race”-tillstånd.

Att använda en formell ansats för sign-off före syntesen kan spara in en hel del både tid och resurser. En intuitiv GUI-avbuggare kan hjälpa användaren att hitta en bakomliggande orsak till problemen så tidigt som möjligt.

Vi kommer att utforska och analysera resultaten från denna formella metodik på en konstruktion från MaxLinear. Artikeln kommer att beskriva den metodik som MaxLinear använde för att uppnå pålitlig sign-off och hög kvalitet. Vi diskuterar hur teknologin kan användas av konstruktörerna för designvalidering under de tidigaste stegen av produktutvecklingen och föreslå förbättringar av teknologin och metodiken.

Formella tekniker är väl etablerade som en väsentlig del av funktionell verifiering av hårdvarukonstruktioner. Många konstruktörer har gått över till SystemC/C++ för att höja abstraktionsnivån och uppnå fördelarna med syntes på högnivå. Denna ansats snabbar upp designprocessen av hårdvaran, men med fokus på källkod för SystemC/C++ och inte på RTL-design efter HLS.

Fig 1. SystemC/C++ High-Level designflöde

II. DEN REKOMMENDERADE METODIKEN
Den helt automatiserade funktionaliteten hos den formella metodiken för verifiering av konstruktioner i SystemC/C++ har använts för en konstruktion från MaxLinear. Helt funktionell, assertion-baserad formell verifiering gjorde att omfattande assertions kunde testas mot designkod i SystemC/C++. Dessa assertions skrev med hjälp av enkla C-assert-statements, för full System Verilog Assertions (SVA) med alla temporala, samtidiga konstruktionsidéer inkluderade. En unik egenskap hos den använda teknologin är möjligheten att dra nytta av temporala assertions på konstruktioner i SystemC/C++.

Flera olika testmotorer som utnyttjar ett antal standardiserade och företagsspecifika algoritmer användes för att åstadkomma en djupgående kodanalys. Denna metod uppvisar genomgående en hög grad av konvergens jämfört med andra lösningar, och detta tillsammans med snabb operation med hög kapacitet. Att använda en bra avbuggningsmiljö gav en klar väg mot att snabbt spåra problem med konstruktioner och tester.

Den automatiserade teknologin användes på hårdvarudesignkod i SystemC/C++ för att eliminera buggar tidigt under designprocessen. En full uppsättning av automatiserade kontroller användes för att få fram djupgående statisk analys av designkoden. Denna teknik hjälpte till att eliminera behovet av manuellt skrivna assertions.

Inspektionsteknologin sökte efter potentiella buggar genom att analysera operationella scenarier baserade på kodkonstruktionen. Säkerhetskontroller, som access utanför gränserna till en array eller låsning av en tillståndsmaskin, aktiveringskontroller samt strukturell analys inklusive klassiska missanpassningar mellan simulering och syntesoperation, fanns direkt tillgängliga.

Det var viktigt att kontrollera vilka register som explicit initierades. SystemC-variabler initieras automatiskt vid simulering, men HLS-verktyg (High Level Synthesis) ignorerar dessa. Detta leder till missanpassningar mellan simulering och syntes som är svåra att avbugga. Verifieringsteamen kontrollerade också om icke initierade register, odefinierade operationer eller multipla drivenheter kan sprida X (okända) värden i konstruktionen. Det finns inte någon indikation av okända värden vid SystemC-simulering, så det krävs formell analys för att upptäcka propageringsproblem. SystemC saknar också icke-blockerande assignments, vilket leder till race-tillstånd och missanpassningar mellan sekventiell simuleringssemantik och parallell operation i hårdvaran.

Många av de problem som fångas upp med hjälp av denna metodik kontrolleras inte vid simulering av HLS. Här finns oavsiktligt beteende vållat av problem med specifika datatyper, t.ex. för fasttalsaritmetik, samt problem med samtidighet som utvärdering av race-tillstånd.

Denna teknik accepterar majoriteten av SystemC-funktioner. Det gör att assertions kan testas mot ett antal olika kodabstraktioner, från transaction10level-modeller (TLM) över detaljerade RTL (Register Transfer Level) och ner till nätlistan, och från obegränsade till fullständiga, cykel-noggranna representationer.

Fig 2. Användande av SystemVerilog Assertions med en SystemC/C++-konstruktion

Både enkla ANSI C-assertions och fullt temporala, samtidiga SVA (System Verilog Assertions) kan användas med konstruktioner i SystemC/C++. Denna flexibilitet vid beskrivningen av assertions gör att befintliga assertions för andra konstruktioner kan återanvändas eller utnyttjas som mallar, vilket minskar den upplärningskostnad som ett nytt format medför. Detta ger också möjligheter att uppnå ett konsekvent flöde före och efter syntes, där samma assertions – om de skrivits med flödet i tankarna – kan återanvändas på ”golden models” i SystemC/C++ och deras RTL-syntetiserade avledningar. Dessutom kan uppsättningar av VIP-assertions (Verification Intellectual Property) som skapas för RTL-miljöer, t.ex. en verifierare av bussprotokoll, återanvändas på kod i SystemC/C++.

Metodiken tillåter sekventiella assertions, som kan användas för att beskriva specifikationselement, förväntade konstruktionsegenskaper och feltillstånd som skall testas mot abstrakt kod. Detta ger ingenjörerna möjlighet att arbeta på SystemC/C++-nivå i sina ”golden designs” för att kunna garantera att de klarar specifikationerna före syntesen. Detta möjliggör en omfattande, formell lösning på en nivå där specifikationerna kan spelas mot olika val av mikroarkitektur. Slutligen omöjliggör den knepet att avbugga en SystemC/C++-konstruktion genom att använda den redan syntetiserade RTL-koden.

Fig 3. En omfattande uppsättning av kontroller för SystemC/C++-kod

III. I PRAKTIKEN
Som tidigare nämnts har den beskrivna metodiken testats tillsammans med MaxLinear på en ny konstruktion.

Teknologin och metodiken användes på konstruktionens högsta nivå, och inte på specifika moduler. Implementeringen utfördes i syfte att snabba upp den totala verifieringsprocessen och att köra en verifiering på den motsvarande nivån av den konstruktion som senare skall användas i HLS-processen. Nedan beskrivs också en annan möjlig applikation som använder submoduler och hierarkier, men denna kräver potentiella begränsningar av indata för att reproducera det subset av värden som andra submoduler driver.

Det QLNW-flöde användes som integrerats i verifieringsskript. QLNW står för ”Quick, Lunch, Night and Weekend runs”. Det är ett intuitivt och enkelt sätt att utnyttja procedurer som använts för att utföra verifieringskontroll i den motsvarande tidsramen (Q=15 min, L=1 h, N=12 h, W=48 h). Det implementeras för maximalt utbyte när det gäller att uppnå så många konvergerande kontroller som möjligt inom den korta körningstiden.

Basala tester i GUI-mod utfördes för att filtrera ut icke viktiga kontroller och köra de erforderliga kontrollerna. Dessutom utfiltreras vissa grupper av kontroller som ursprungligen kom från filer som redan verifierats.

De misslyckade kontroller som rapporterats avbuggades sedan med GUI-avbuggaren. Denna arbetar intuitivt och kan visa aktiv kod i den valda tidsramen med vågformerna hos de relaterade signalerna. Med den aktiva koden kunde användaren följa värden med en spårningsfunktion för att hitta den bakomliggande orsaken till dessa problem i designkoden. Dessa kontroller återkördes sedan för att garantera att det inte fanns några ytterligare felande kontroller.

IV. RESULTAT
Ett antal problem med trunkerade värden och värden utanför tillåtna gränser hittades med den föreslagna metodiken. Dessa problem hittas med Quick+Lunch-procedurer och motsvarar verkliga designbuggar. Detta gäller speciellt för fel med värden utanför gränserna som var svåra att upptäcka med andra tekniker. Teamet på MaxLinear använde den automatiserade lösningen OneSpin SystemC Inspect för att uppnå dessa resultat. Om dessa problem inte hade hittats i SystemC-koden hade det varit svårt att hitta dem med vanliga simuleringsbaserade tekniker eftersom simulering inte kan garantera 100 procents täckningsgrad. Formell verifiering kan göra en ingående analys och ta fram de rätta kontrollerna för att uppnå 100 procents täckning för driver- och input-stimulus.

V. FRAMTIDEN
MaxLinear planerar att använda dessa formella tekniker för pre-design-fasen i framtida projekt. Man tror att detta drastiskt kommer att förkorta verifierings- och avbuggningstiderna och leda till mer funktionellt korrekta och säkra konstruktioner.

Nästa steg är att integrera OneSpins teknologi för SystemC-verifiering i andra projekt, och att utföra extra analyser och kontroller med de nya funktioner som finns tillgängliga med de senaste OneSpin-versionerna från 2021.2. Bland dessa funktioner finns överskrivning av processer (signalen skrivs in flera gånger under 1 klockperiod i en och samma process) samt läs-före-skriv (signalen avläses innan den skrivs).

Vlada Kalinic, produktchef för SystemC Formal Verification på OneSpin, ett Siemens-företag

Filed under: EDA