Técnicas de verificación funcional de sistemas digitales

Resumen

En la tesis se desarrollan varias técnicas de verificación de sistemas digitales a nivel funcional. Las técnicas parten de un modelo funcional que permite describir sistemas atemporales con tipos de datos y construcciones de control complejas. La metodología de modelado está basada en sistemas de inecuaciones de tipo polinomial. La primera área de investigación explora técnicas estáticas de generación de vectores de entrada en procesos de verificación basados en aserciones. El objetivo de las técnicas desarrolladas es encontrar patrones de entrada que no cumplan las aserciones que modelan el funcionamiento del sistema o las restricciones de entrada/salida. La primera técnica desarrollada esta basada en análisis de intervalos modificado (MODIA) que mejora en eficiencia a las técnicas de análisis de intervalos tradicionales. La segunda técnica explora la utilización de herramientas de optimización no-lineal frente a técnicas que utilizan herramientas de optimización lineal. La principal ventaja es que trabajan en el dominio real (mayor rapidez de convergencia) y permiten manejar operadores no lineales (multiplicación) sin necesidad de aplicar transformaciones para convertirla en un conjunto de operadores lineales. La segunda área de investigación se centra en la verificación basada en simulación. La primera aportación se centra en conocer la capacidad de detección de fallos de las métricas tradicionales de cobertura (código, saltos, bloque). Y la segunda, en mejorar el conjunto de vectores de prueba para la verificación de sistemas complejos. La primera parte provee a las métricas de cobertura utilizadas en simulación de un significado formal. El trabajo proporciona ecuaciones que permiten cuantificar la calidad de las métricas de cobertura de camino, de bloque y de sentencias. La principal conclusión es que dichas las métricas proporcionan una capacidad alta de detección de errores si los rangos de entrada son suficientemente grandes. Con respecto a las sentencias de control, la principal conclusión es que la cobertura de errores de dicha métrica es baja (aproximadamente un 50%). Otra conclusión es la evaluación de la complejidad de la verificación exhaustiva de sistemas descritos a nivel funcional. Esta complejidad depende del grado de los polinomios (complejidad de la descripción) y del número de entradas, por lo que transformaciones que incrementan estos valores (por ejemplo, la conversión de entradas de tipo entero a un vector de bits) pueden tener un impacto negativo sobre la complejidad de la verificación. La segunda parte de esta área es la mejora de la generación automática de vectores para simulaciones aleatorias. Los puntos clave son, por un lado, aprovechar la información que se obtiene de la propia simulación, y por otro lado, definir vectores capaces de ejecutar los dos caminos de las sentencias condicionales (100% de cobertura de saltos). En resumen, esta Tesis ha abordado dos líneas de trabajo, definiendo 4 técnicas de verificación semi-formal y dando lugar a 16 publicaciones en congresos internacionales y una revista.