This thesis goes around the effort made to verify a submodule of a vector processing unit or VPU. This submodule is the one in charge of performing vector reductions, and due to the nature of some of the reductions, an extra effort was needed in order to correctly verify the correct functioning of it. These efforts can be divided into three main objectives: creating a specific reference model for these reductions, which will be used along-side an existing reference model that is being used to verify the whole VPU, creating a set of assertions to check the adherence of this submodule to the specifications, since these assertions are going to target, mainly, the interface of this submodule, and working on the coverage, which will also focus on the inputs to this submodule, making sure that all the possible corner cases and base cases known are met.
Aquesta tesi es basa en el esforços realitzats per a la verificació d'un submòdul d'una unitat de processament de vectors o VPU. Aquest submòdul és l'encarregat d'efectuar reduccions vectorials i, a causa de la naturalesa d'algunes d'aquestes reduccions, es necessita un esforç extra per a verificar el seu correcte funcionament. Aquests esforços es poden dividir en tres objectius principals: la creació d'un model de referencia específic per aquestes reduccions, el qual es farà servir juntament amb un model de referencia existent que es fa servir per a verificar la VPU sencera, la creació d'un conjunt d'assercions per a corroborar l'adequació d'aquest submòdul, i la cobertura (coverage en anglès), la qual tambè estarà enfocada en las senyals d'entrada d'aquest submòdul, assegurant que tots els casos especials i els casos base són coneguts i es donen.
Esta tesis se basa en los esfuerzos ralizados para la verificación de un submódulo de una unidad
de procesamiento de vectores o VPU. Este submódulo es el encargado de efectuar reducciones
vectoriales y, debido a la naturaleza de algunas de estas reducciones, se necesita
un esfuerzo extra para verificar su correcto funcionamiento. Estos esfuerzos se pueden dividir
en tres objetivos principales: la creación de un modelo de referencia específico para estas
reducciones, el cual se usará junto a un modelo de referencia existente que se usa para verificar
la VPU entera, la creación de un conjunto de aserciones para corroborar la adequación
de este submódulo a sus especificaciones, ya que estas aserciones estarán enfocadas especialmente
a la interfaz de este submódulo, y la cobertura (coverage en inglés), la cual también
estará enfocada en las señales de entrada de este submódulo, asegurando que todos los ca-
sos especiales y casos base son conocidos y se dan.
