polito.it
Politecnico di Torino (logo)

Functional and Formal Verification on submodules of a Vector Processing Unit based on RISC-V V-extension

Vito Luca Guglielmi

Functional and Formal Verification on submodules of a Vector Processing Unit based on RISC-V V-extension.

Rel. Luciano Lavagno. Politecnico di Torino, Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering), 2020

[img]
Preview
PDF (Tesi_di_laurea) - Tesi
Licenza: Creative Commons Attribution Non-commercial No Derivatives.

Download (2MB) | Preview
Abstract:

This thesis was developed while working at Barcelona Supercomputing Center, a research center specialized in High Performance Computing and investigation in many fields, such as cloud computing, bioinformatics, material science and more. Taking part to European Processor Initiative (EPI) project, the whole thesis aims to perform the verification process on a Vector Processing Unit (VPU). The implemented Vector Processing Unit is based on the RISC-V V-Extension, which is a set of specifications defining the Instructions Set Architecture (ISA) of a vector core. The V-Extension is currently on develop by the RISC-V foundation. This manuscript will refer to the versions 0.7.1. The first chapter consist of an introduction of the needed concepts and of the context in which this thesis is been developed. Then, in the second chapter, all the techniques used to verify functionally and formally this VPU are discussed. All the results, such as found bugs or created material, are displayed in the third chapter. Moreover, analysing these results, the efficacy of the techniques used is evaluated. It is shown how formal and functional tools can be used to find bugs or to better define specification. In the last chapter, it is possible to conclude that the techniques adopted produced the expected results showing significant improvements in the verification effort.

Relatori: Luciano Lavagno
Anno accademico: 2020/21
Tipo di pubblicazione: Elettronica
Numero di pagine: 109
Soggetti:
Corso di laurea: Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering)
Classe di laurea: Nuovo ordinamento > Laurea magistrale > LM-29 - INGEGNERIA ELETTRONICA
Ente in cotutela: UNIVERSIDAD POLITECNICA DE CATALUNYA - ETSET BARCELONA (SPAGNA)
Aziende collaboratrici: BARCELONA SUPERCOMPUTING CENTER
URI: http://webthesis.biblio.polito.it/id/eprint/16044
Modifica (riservato agli operatori) Modifica (riservato agli operatori)