Diseño de un ambiente de verificación formal basado en SystemVerilog Assertions para una unidad aritmética lógica de punto flotante

Abstract

Este proyecto desarrolla un entorno de verificación formal para la unidad aritmética lógica de punto flotante (FPU) del microcontrolador SIWA. Se requiere validar la ALU exhaustivamente antes de integrarla al estándar RISC-V con extensión F. La verificación se realizó con SystemVerilog Assertions y VC Formal, siguiendo un enfoque grey box para evaluar cada etapa interna del sumador y del multiplicador en precisión simple IEEE-754. Se definieron aserciones para comprobar el correcto desempaquetado, alineamiento de exponentes, suma y resta de mantisas, normalización, redondeo, empaquetado y manejo de excepciones. El entorno permitió identificar fallos funcionales y validar comportamientos críticos como overflow, underflow y NaN. El resultado es un flujo estructurado y reproducible que fortalece la confiabilidad del diseño y sienta la base para futuras verificaciones de la FPU completa.This project develops a formal verification environment for the floating-point arithmetic logic unit (FPU) of the SIWA microcontroller. The ALU must be thoroughly validated before being integrated into the RISC-V standard with the F extension. The verification was performed using SystemVerilog Assertions and VC Formal, following a grey-box approach to evaluate each internal stage of the adder and multiplier in IEEE-754 single precision. Assertions were defined to check correct unpacking, exponent alignment, mantissa addition and subtraction, normalization, rounding, packing, and exception handling. The environment enabled the identification of functional failures and the validation of critical behaviors such as overflow, underflow, and NaN. The result is a structured and reproducible flow that strengthens the design’s reliability and establishes the foundation for future verification of the complete FPU.