Functional and formal verification on submodules of a vector processing unit based on RISC-V V-extension

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.