Formal Verification Techniques to Check Functional Equivalence between High-Level C Models and RTL Implementations using Jasper C2RTL
Gaetano Maria Raia
Formal Verification Techniques to Check Functional Equivalence between High-Level C Models and RTL Implementations using Jasper C2RTL.
Rel. Maurizio Martina. Politecnico di Torino, Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering), 2023
Abstract
The pervasiveness of digital systems in almost all commercial and industrial sectors has led to increased productivity and reduced time-to-market. Moreover, due to the complexity of modern Very Large Scale Integration (VLSI) designs, various verification techniques have been developed to cope with undetected functional failures. As a complement to traditional dynamic simulations, Formal Verification (FV) offers the possibility to mathematically check the functional correctness of the Device Under Verification (DUV) in a drastically shortened time, along with exhaustive coverage of the design state space. Formal Equivalence Verification (FEV) consists in comparing two models, known as specification and implementation, to check whether they are functionally equivalent or not.
Although traditionally a similar verification methodology has been employed for RTL-versus-RTL and RTL-versus-netlist scenarios, thanks to the recent improvements in formal engines solving capabilities, nowadays one can perform C-versus-RTL equivalence
Tipo di pubblicazione
URI
 |
Modifica (riservato agli operatori) |
