Model vs RTL : correlation beyond testing. Exploring the use of C vs RTL formal equivalence techinques for verification of CPU designs.

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.