
Demetrio Bori
Model vs RTL : correlation beyond testing. Exploring the use of C vs RTL formal equivalence techinques for verification of CPU designs.
Rel. Paolo Enrico Camurati. Politecnico di Torino, Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering), 2023
Abstract: |
Nel campo della progettazione moderna della CPU il flusso di lavoro di sviluppo vede nei primi passi la descrizione di un modello algoritmico di alto livello da cui i progettisti prenderanno ispirazione per produrre un'implementazione RTL capace di soddisfare idealmente queste specifiche di riferimento i. Potenti tecniche vengono utilizzate oggi per verificare questi CPU designs e la verifica formale fornisce un grande livello di fiducia durante l'analisi sulla correttezza delle nostre implementazioni. Mentre la capacità di descrivere proprietà interessanti scrivendo asserzioni e covers possono essere cruciali per verificare i nostri designs, l'uso delle tecniche formali di equivalenza sembra adeguato all'obiettivo di correlare il modello di riferimento algoritmico con l'implementazione RTL. L'applicazione JasperGold C2RTL fornisce le caratteristiche e strutture necessarie per implementare questo tipo di flusso di verifica e consentirà per avere una conoscenza più completa del nostro design. Il lavoro discusso in questo documento mira a valutare l'efficienza di questo tipo di approccio quando si tratta di vari tipi di design , passando da casi semplici logica combinatoria a casi più complessi , con l'aggiunta di elementi sequenziali tenendo sempre conto delle possibili tecniche per ridurre la complessità. L'organizzazione del lavoro è la seguente: concetti di base sui i metodi formali e di verifica , comprese le aspetti di analisi della complessità e Formal equivalence Verification . Il secondo capitolo approfondisce in materia di verifica formale l'approccio C vs RTL e da una veloce introduzione all'uso di JasperGold C2RTL App. Il terzo capitolo copre i primi due casi di prova , relativi a i concetti di equivalenza combinatoria ; mentre il quarto capitolo copre i principali testcases e l'indagine dello strumento quando si lavora con design sequenziali. Il quinto capitolo conclude il lavoro con un riferimento ad un ultimo progetto in prova e dis- discussione su lavori futuri. |
---|---|
Relators: | Paolo Enrico Camurati |
Academic year: | 2022/23 |
Publication type: | Electronic |
Number of Pages: | 68 |
Additional Information: | Tesi secretata. Fulltext non presente |
Subjects: | |
Corso di laurea: | Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering) |
Classe di laurea: | New organization > Master science > LM-29 - ELECTRONIC ENGINEERING |
Ente in cotutela: | INSTITUT EURECOM (FRANCIA) |
Aziende collaboratrici: | ARM France SAS |
URI: | http://webthesis.biblio.polito.it/id/eprint/26679 |
![]() |
Modify record (reserved for operators) |