Sai per certo che il tuo RISC-V RTL non contiene sorprese?

Data la relativa novità e complessità dei progetti RISC-V RTL, sia che tu stia acquistando un core supportato commercialmente o scaricando una popolare offerta open source, c'è il rischio piccolo ma diverso da zero che sorprese indesiderate sfuggano al tuo prodotto finale. In ordine di probabilità dal più alto al più basso, considera:

• La presenza di un bug strano ma del tutto possibile
• Bug "all'interno" delle istruzioni personalizzate che tu o il tuo fornitore state creando per la vostra applicazione
• Bug "ai margini" di un'istruzione personalizzata, ad esempio l'istruzione viene eseguita correttamente, ma in qualche modo lascia la macchina in uno stato danneggiato
• Correlati: nuove funzionalità non documentate e/o scarsamente specificate che inconsapevolmente aprono buchi nel progetto
• Logica trojan dannosa inserita di nascosto tramite un attacco alla catena di approvvigionamento

Approcci di mitigazione comuni

Naturalmente, la prima linea di difesa è l'ispezione esperta del codice RTL in arrivo o in via di sviluppo. Ovviamente, questo dovrebbe essere fatto; ma dovrebbe essere altrettanto ovvio che questa tecnica - come si dice nel mondo matematico - "è necessaria ma non sufficiente" (anche se hai fatto rivedere il tuo codice dal professor Patterson in persona).

La prossima linea di difesa sta applicando approcci basati sulla simulazione: Instruction Set Simulation (ISS), confronto automatizzato del tuo DUT con modelli golden maturi, banchi di prova UVM casuali vincolati per la simulazione DUT RTL e persino convogliare lo stimolo del mondo reale nell'emulazione assistita dall'hardware del DUT. Ancora una volta, questi approcci sono tutti preziosi e dovrebbero essere fatti; ma soffrono tutti dello stesso difetto: sono intrinsecamente incompleti poiché si basano sulla generazione di stimoli. Ad esempio, nel caso estremo ma possibile di un attacco alla catena di approvvigionamento, lo sviluppatore della logica del trojan ha deliberatamente creato una sequenza di attivazione di segnali e dati che probabilmente sfuggirà al rilevamento anche del più creativo hacker white hat. E, naturalmente, i bug funzionali hanno il loro modo di utilizzare l'entropia presente in natura per rimanere nascosti.

La linea di fondo è che l'unico modo per essere completamente sicuri che il tuo RISC-V RTL sia privo di sorprese naturali o dannose è applicare metodi formali esaustivi per verificare il design.

Più facile a dirsi che a farsi, vero?

Sì e no: 14 anni fa, questo tipo di analisi era fattibile solo da ricercatori a livello di dottorato utilizzando i propri programmi fatti a mano. Ma dal 2008, gli strumenti e le tecniche sono stati prodotti in modo tale che chiunque abbia familiarità con le basi della verifica formale e la scrittura dello standard IEEE System Verilog Assertions (SVA) possa applicare rapidamente e avere successo qui.

Un processo formale in tre fasi

Il flusso consigliato su base formale si sviluppa come segue:

1. Crea un banco di prova formale che "modelli" la specifica DUT
2. Definire i vincoli di input e i controlli da eseguire rispetto al DUT
3. Eseguire analisi

Passaggio 1: creare un banco di prova formale che "modelli" la specifica DUT

La base di questa metodologia consiste nello scrivere un insieme di proprietà che rappresentano il comportamento di ciascuna istruzione nella progettazione RISC-V. Il compito è catturare l'effetto di una data istruzione sugli output dell'IP e sugli stati dell'architettura interna (nel mondo RISC-V, questo è il program counter (PC) e register file (RF)) per ogni data sequenza di input arbitrariamente lunga. Questo viene fatto utilizzando un'estensione appositamente creata per IEEE SVA chiamata Operational SVA. In poche parole, questa è una libreria fornita con lo strumento di verifica del processore basato su formali; e dal punto di vista dell'ingegnere di verifica, sembra un sottoinsieme intuitivo del codice SVA familiare. La figura 1 mostra la struttura generica:

proprietà istruzione_A; // stato concettuale t ##0 ready_to_issue() e // trigger t ##0 opcode==instr_A_opc implica // stato concettuale t ##0 ready_to_issue() e // output delle interfacce di memoria // lettura dell'istruzione successiva t ##0 imem_access(instr_A_opc) e // data load/store t ##1 dmem_access(instr_A_opc) e // registri architetturali t ##1 RF_update(instr_A_opc) e t ##1 PC_update(instr_A_opc) endproperty 

Fig. 1: Struttura del codice SVA operativo che cattura la specifica di un'istruzione del processore. [1]

Facendo riferimento alla figura 1, il lato sinistro del coinvolgimento (la parte di codice sopra la parola chiave implica) identifica quando la macchina è pronta per emettere una nuova istruzione e l'istruzione viene emessa. L'asserzione cattura i valori correnti degli stati dell'architettura e, nella parte destra dell'implicazione (porzione di codice sotto la parola chiave implica), dimostra i loro prossimi valori.

Inoltre, le uscite del processore devono essere dimostrate corrette, in questo caso per assicurarsi che l'istruzione acceda ai dati previsti e alle posizioni di memoria delle istruzioni. L'asserzione dimostra anche che la macchina è pronta per emettere una nuova istruzione nel ciclo successivo. Questo è fondamentale per disaccoppiare la verifica di un'istruzione dalla sequenza di istruzioni di cui potrebbe far parte. Ad esempio, l'istruzione A potrebbe essere eseguita correttamente, ma lasciare la macchina in uno stato danneggiato. Questo stato errato potrebbe far sì che l'istruzione successiva B produca risultati errati non per colpa sua. Quindi, con l'approccio Operational SVA, l'istruzione di verifica dell'asserzione B passerebbe, mentre l'istruzione di verifica dell'asserzione A fallirebbe (dove le operazioni di lettura e scrittura della memoria potrebbero durare diversi cicli).

In conclusione: le funzioni che rappresentano gli stati architetturali nel codice SVA operativo devono essere mappate ai segnali di implementazione e devono riflettere la microarchitettura del processore. Lo stato della RF, ad esempio, potrebbe dipendere dall'attivazione dei percorsi di inoltro. [1]

[Nota: per quelli di voi che hanno familiarità con la simulazione o la copertura funzionale formale, questa nozione di completezza non si basa su metriche di copertura strutturale o sulla creazione e raccolta di metriche per un modello di copertura funzionale. Invece (e anticipando leggermente i passaggi e i risultati rimanenti), l'output dell'analisi qui riguarda l'ottenimento di prove complete per tutte le proprietà. Le prove complete mostrano anche implicitamente che non esiste altra funzionalità, non specificata o inaspettata (spec o bug di codifica) o inserita in modo dannoso, che non viene acquisita da questo insieme di proprietà. Riformulando, questa metodologia si basa sul raggiungimento del 100% di "copertura del piano di test" come verificato dai risultati esaustivi dell'analisi formale - dove nulla è più "completo" di una dimostrazione matematica!]

Passaggio 2: definire i vincoli di input e i controlli da eseguire rispetto al DUT

Per completare le proprietà di specifica per ciascuna istruzione, il passaggio successivo consiste nel definire i vincoli di input e gli eventuali controlli di output aggiuntivi. Ancora una volta, viene impiegato SVA operativo, in cui l'utente ora specifica un "piano di completezza" per definire sia gli input legali che la segnalazione illegale che il DUT dovrebbe ignorare. Per l'esempio mostrato nella figura 2, ci sono tre sezioni: ipotesi di determinazione, requisiti di determinazione e grafico delle proprietà.

processore di completezza; presupposti_determinazione: // INGRESSI determinati(imem_data_i); determinato(dmem_valid_i); if (dmem_valid_i) determinato(dmem_data_i) endif; determinazione_requisiti: // USCITE determinate(imem_read_o), if (imem_read_o) determinate(imem_addr_o) endif; determinato(dmem_enable_o); if (dmem_enable_o) determinato(dmem_rd_wr_o), determinato(dmem_addr_o) endif; // STATI ARCHITETTONICI determinati(PC); determinato(RF); property_graph: all_instructions := instruction_not_a, instruction_add_a, instruction_sub_a, [...] all_instructions -> all_instructions; terminare la completezza; 

Fig. 2: Esempio di un piano di completezza con presupposti e requisiti di determinazione condizionale.

Elaborare:

• "determination_assumptions" è semplicemente un nome di fantasia per i vincoli del valore di input
• "determination_requirements" è una definizione dei segnali che devono essere verificati (sia i segnali di uscita del processore che gli stati architetturali)
• La sezione "property_graph" è semplicemente un'associazione di questo file a tutte le proprietà create nel passaggio 1

Ricapitolando dove siamo a questo punto: nel passaggio 1 hai creato quello che è effettivamente un modello accurato del ciclo del DUT che deve essere dimostrato vero per tutto il tempo e tutti gli input; nel passaggio 2 si impostano i vincoli e gli eventuali comportamenti speciali a cui prestare attenzione. Aggiungili insieme e in effetti hai un banco di prova formale pronto per essere eseguito!

Passaggio 3: eseguire l'analisi

L'obiettivo di tutti gli strumenti formali è dimostrare in modo esaustivo che tutte le proprietà sono vere per tutto il tempo e per tutti gli input. Nel caso della verifica del processore RISC-V, lo strumento funziona per dimostrare che qualsiasi sequenza di input arbitrariamente lunga può essere abbinata a una sequenza univoca dello SVA operativo specificato che prevede i valori degli output e degli stati dell'architettura.

E questo è esattamente ciò che accade. Se viene rilevata una differenza di comportamento tra la specifica e il DUT, lo strumento formale fornisce una forma d'onda di "controesempio" che mostra esattamente la serie di segnali di input e dati che possono creare una violazione della specifica. Come accennato in precedenza, tali fallimenti possono essere trovati all'interno della logica RTL dell'istruzione o nella "logica di trasferimento" che avvia il successivo ramo/istruzione legale.

Ad ogni modo, quando questi problemi vengono risolti e lo strumento dimostra tutte le proprietà, i risultati sono veramente "completi" — ovvero, puoi essere matematicamente certo che non ci sono errori di codifica RTL — l'analisi formale ha letteralmente dimostrato l'assenza di bug !

Risultati

Innanzitutto, come notato sopra, nel corso degli anni molti sviluppatori di processori hanno beneficiato di questo flusso [2], [3], [4].

Mettendo alla prova questa metodologia con RISC-V, i miei colleghi hanno realizzato un caso di studio utilizzando il popolare core open source Rocket Chip. Nello specifico è stata esaminata la configurazione RV64IMAFDC – sv39 vm. Si tratta di un core del processore a 64 bit con un sistema di memoria virtuale a 39 bit [5] ed estensioni, come istruzioni compresse e atomiche [6]. Questa implementazione ISA RISC-V open source utilizza una pipeline in ordine a cinque fasi, a problema singolo, con completamento fuori ordine per istruzioni a lunga latenza, come divisioni o cache miss. Il core supporta anche la predizione del ramo e la modifica in fase di esecuzione del registro "misa", consentendogli di disattivare determinate estensioni del set di istruzioni.

Sebbene questa istantanea del Rocket Chip fosse stata ampiamente verificata e registrata più volte, quattro comportamenti sospetti precedentemente sconosciuti, casi limite, sono stati identificati e segnalati agli sviluppatori di Rocket Core RTL. Questi problemi ([7], [8], [9] e [10]) sono stati scoperti esclusivamente attraverso l'applicazione sistematica dell'approccio di verifica formale completo delineato in questo articolo.

Elaborando specificamente [10] - la scoperta di un'istruzione non standard CESARE (codice operativo 0x30500073) nell'RTL: chiaramente il team di Rocket Chip è rimasto indietro con la documentazione (e l'hanno risolto quasi immediatamente dopo aver presentato la richiesta pull di GitHub). Il punto più importante è che ciò dimostra che la logica richiesta per implementare un'intera istruzione - dozzine di righe di codice e molte porte di logica sintetizzata, posizionata e instradata - può sfuggire al rilevamento mediante ispezione visiva, simulazione RTL, simulazione a livello di porta, l'intero processo di implementazione back-end e prototipi hardware in laboratorio!

Ma per quanto riguarda le prestazioni di questo flusso?

Innanzitutto, affrontiamo il significato più ampio di "prestazioni". A causa della natura innovativa del progetto Rocket Chip, per questo caso di studio ci sono volute circa 20 settimane di ingegneria per i nostri professionisti della verifica formale per sviluppare l'intero banco di prova e i vincoli. Tuttavia, le applicazioni precedenti di questo flusso su IP commerciali più strutturati in genere hanno richiesto una frazione di questo tempo. Naturalmente, l'intero processo di presentazione andrà molto più veloce quanto più stabili e mature sono le specifiche, quanto ben documentato e leggibile è il codice DUT RTL e quanto accesso hai ai progettisti per domande e risposte.

Una volta impostato l'ambiente, il tempo di esecuzione dell'orologio da parete era di 2 ore, vale a dire molto meno di quanto ci si potesse ragionevolmente aspettare dalla simulazione RTL casuale vincolata e persino dalla verifica assistita dall'hardware. Inoltre, ricordiamo che i risultati di questa analisi sono validi per tutti gli input e per tutti i tempi - in una parola, sono esaustivi [11].

Sommario

L'approccio completo e formale alla verifica del processore presentato in questo articolo utilizza un'estensione di IEEE SVA, Operational SVA, per verificare formalmente che un ISA RISC-V sia privo di lacune e incoerenze. A differenza dei testbench di simulazione casuali vincolati, dell'emulazione o della prototipazione fisica, l'insieme completo di proprietà e vincoli rileva in modo esaustivo molti tipi di errori RTL, nonché la presenza di codice non documentato o scarsamente specificato e trojan dannosi.

Riferimenti

1 – Conferenza GOMACTech 2019, Albuquerque, Nuovo Messico, 28 marzo 2019: Verifica formale completa degli IP del processore RISC-V per circuiti integrati attendibili senza trojan, David Landoll, et.al.

2 – DVCon 2007: Verifica formale completa di TriCore2 e altri processori, Infineon Gmbh.

3 - 51^st Design Automation Conference (DAC): verifica formale applicata alla piattaforma di progettazione MCU Renesas utilizzando gli strumenti OneSpin

4 – DVCon Europe 2019: Verifica formale completa di una famiglia di DSP automobilistici, Bosch Gmbh.

5 – Manuale del set di istruzioni RISC-V, volume II: architettura privilegiata, versione documento 1.10.

6 Soluzioni https://github.com/freechipsproject/rocket-chip [accesso 20 dicembre 2018]

7 – Risultato dell'istruzione DIV non scritto nel file di registro
https://github.com/freechipsproject/rocket-chip/issues/1752

8 – Istruzioni JAL e JALR Memorizza diversi PC di restituzione
https://github.com/freechipsproject/rocket-chip/issues/1757

9 – Codici operativi illegali riprodotti e causando effetti collaterali imprevisti
https://github.com/freechipsproject/rocket-chip/issues/1861

10 – Istruzione non standard CEASE (Opcode 0x30500073) Scoperta in RTL, https://github.com/freechipsproject/rocket-chip/issues/1868

11 – Verification Horizons blog, Come puoi dire che la verifica formale è esaustiva?, Joe Hupcey III
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/

Fonte: https://semiengineering.com/do-you-know-for-sure-your-risc-v-rtl-doesnt-contain-any-surprises/