Contribuciones a la verificación funcional moderna

Título:

Contribuciones a la verificación funcional moderna

Autor:

Goñi, Oscar

Otros autores / Colaboradores:

 Todorovich, Elías; [ Director/a]  Díaz, Francisco Javier; [ Codirector/a] 

Temas:

DISEÑO DE FRAMEWORKS; 

URL:

https://doi.org/10.35537/10915/49326,

Palabras clave:

verificación de diseños, 

Nota de tesis:

Tesis (Doctorado en Ciencias Informáticas) - Universidad Nacional de La Plata. Facultad de Informática, 2015.

Extensión:

1 archivo (6,3 MB) : il. col.

Resumen:

El incesante desarrollo tecnológico en la industria del silicio y la necesidad de cumplir con tiempos de mercado competitivos han llevado al desarrollo de nuevas técnicas de diseño y verificación funcional. En este trabajo de tesis se presentan diferentes aportes a la verificación funcional moderna partiendo de casos de estudio reales y en donde se plantean diversos problemas a resolver. El trabajo se divide implícitamente en dos partes: La primera, se enfoca en realizar aportes a la verificación funcional proponiendo métodos para generación de entradas, chequeo de salidas y evaluación de cobertura funcional en diseños. En particular, se considera como caso de estudio la verificación funcional de unidades aritméticas sustentándose en la utilización y desarrollo de los frameworks para verificación funcional OVM y Teal and Truss. Del análisis y desarrollo se obtiene un conjunto de reglas para la generación aleatoria de casos de prueba para la verificación de unidades de punto flotante. Ademas, se realiza la evaluación de, no solo el comportamiento de los frameworks propuestos, sino también se analizan parámetros de calidad como su usabilidad, extensibilidad y nivel de abstracción. Como aporte se describen los pasos para diseñar e implementar monitores de verificación aplicables a diversos dominios. El monitor presentado, no solo realiza el chequeo de resultados comparados con modelos de referencia, sino que ademas realiza el análisis de cobertura considerando los casos ejercitados. En la evaluación de los frameworks se verifican dos diseños diferentes de unidades aritméticas donde al menos se detectan dos errores en casos no considerados por parte del diseñador. La segunda parte del trabajo propone un nuevo enfoque para la verificación funcional. El enfoque propuesto parte del hecho que las pruebas orientadas a la verificación deben realizarse indefectiblemente en todo proyecto y propone preparar a los entornos de verificación de manera tal que sus resultados sean de utilidad para el diseñador. Como caso de estudio se presenta la verificación de un modelo digital de un convertidor de potencia para emulación HIL (Hardware in the Loop). En particular, se hace énfasis en la aceleración obtenida al utilizar las técnicas de HIL en la verificación de diseños analógicos-digitales. Continuando con la linea de aritmética presentada en la primer sección, primero se compara el comportamiento de un modelo que utiliza punto fijo para la representación de variables de estado con otro que utiliza representación en punto flotante. La evaluación se realiza considerando diversos escenarios representativos y reales donde se aplicaría el convertidor. Luego de comprobar la funcionalidad del convertidor utilizando técnicas descriptas en la primer parte de la tesis, se utilizan los resultados recopilados para el análisis de resolución de dos variables de estados en el modelo de convertidor de punto fijo. La motivación principal de este análisis es que partiendo de resoluciones óptimas es posible obtener modelos que minimizan el área ocupada en el diseño final y la máxima velocidad de reloj del circuito. A partir de los resultados obtenidos, el diseñador puede apreciar que el aumento de resolución a partir de cierto umbral solo incrementa el área utilizada y reduce la frecuencia de reloj sin obtener mejoras significativas en la precisión. Para el caso de estudio evaluado, es posible apreciar que existe un pequeño intervalo de resolución crítico de las variables de estado donde los errores se reducen drásticamente a cero, sin reducción de la performance o aumentar el consumo de área. Si bien en este trabajo, los resultados completos de las pruebas se presentan en un apéndice, el enfoque propuesto resume un gran volumen de información en gráficas de rápida interpretación por parte del diseñador.

Puede solicitar más fácilmente el ejemplar con: TES 15/69

1. Introducción
1.1. El proceso de verificación funcional 
1.2. Interacción dentro del desarrollo de un proyecto 
1.3. Organización del trabajo

2. Fundamentos 
2.1. Verificación funcional tradicional 
2.1.1. Verificación basado en integración
2.1.2. Verificación de microprocesadores 
2.1.3. Emulación y aceleración
2.2. Elementos de la verificación funcional moderna 
2.2.1. Generación aleatoria con restricciones
2.2.2. Programación orientada a objetos en verificación funcional 
2.2.3. Frameworks para verificación funcional 
2.2.4. Aserciones 
2.3. Verificación basada en aserciones 
2.3.1. Inicios
2.3.2. Introducción en la industria 
2.3.3. Verificación dirigida por la cobertura 
2.4. Conclusiones del capítulo 

3. Experiencias aplicando Frameworks para Verificación Funcional en unidades de punto flotante 
3.1. Introducción
3.2. Trabajo relacionado 
3.3. El estándar IEEE754-2008
3.3.1. Formatos 
3.3.2. Conjuntos de datos de punto flotante
3.3.3. Estrategias de redondeo 
3.3.4. Aritmética infinita 
3.3.5. Operaciones con NaNs 
3.4. Diseño de un Sumador/Restador IEEE754-2008 
3.5. Plan de verificación
3.6. Instanciación de los frameworks 
3.6.1. Truss 
3.6.2. OVM
3.6.3. Modelo de referencia 
3.7. Resultados 
3.7.1. Resultados de la verificación funcional 
3.7.2. Evaluación de la experiencia 
3.8. Conclusiones del capítulo 

4. Diseño metodológico de monitores de verificación para unidades de punto flotante 
4.1. Trabajo relacionado 
4.2. El mecanismo de verificación
4.2.1. Monitor de Verificación
4.2.2. Generación de entradas 
4.3. Caso de estudio: Suma y Resta 
4.3.1. Estructura del generador 
4.3.2. Definición de puntos de cobertura 
4.4. Implementación
4.4.1. Implementación del modulo generador 
4.4.2. Implementación del colector de cobertura 
4.4.3. Implementación del módulo Checker
4.4.4. Instantiación dentro de Frameworks de Verificación
4.5. Evaluación de los componentes de verificación
4.5.1. Configuración del Test 1 
4.5.2. Configuración del Test 2 
4.6. Conclusiones del capitulo 

5. Verificación automatizada 
5.1. Introducción
5.2. Generación automatizada de casos de prueba 
5.3. Automatización mediante Scripts 
5.3.1. Automatización mediante componentes de verificación
5.4. Análisis automatizado de resultados
5.4.1. Análisis mediante Scripts 
5.4.2. Análisis mediante componentes de verificación
5.4.3. Nivel Transacción
5.4.4. Nivel Secuencia 
5.4.5. Nivel Test 
5.4.6. Nivel Escenario 
5.5. Caso de estudio: Verificación de modelos HIL para convertidores de potencia 
5.5.1. Motivación 
5.6. Breve reseña de Modelos HIL
5.7. Verificación del BoostConverter QXY 
5.7.1. Breve reseña del formato QXY 
5.7.2. Interface
5.7.3. Sequencer
5.7.4. Driver
5.7.5. DUV 
5.7.6. Monitor 
5.7.7. Scoreboard 
5.7.8. Transacciones 
5.8. Verificación con OVM del convertidor a lazo abierto
5.8.1. Scoreboard
5.8.2. Driver 
5.8.3. Monitor 
5.8.4. Definición de escenarios
5.8.5. Scripts 
5.9. Resultados 
5.9.1. Cobertura de código 
5.9.2. Profiling
5.10. Conclusiones del capítulo 

6. Análisis de resolución asistido por la Verificación funcional 
6.1. Introducción
6.1.1. El problema de la resolución
6.2. Método 1 - Enfoque basado en simulación
6.3. Método 2 - Enfoque analítico 
6.4. Resultados
6.4.1. Escenarios de prueba 
6.4.2. Análisis de área y frecuencia
6.4.3. Resultados del Método 1
6.4.4. Resultados del Método 2 
6.5. Conclusiones del capitulo 

7. Conclusiones del trabajo 
7.1. La interminable tarea de verificación
7.2. Un nuevo enfoque de la verificación
7.3. Producción surgida del presente trabajo de tesis
7.4. Trabajo futuro

A. Verificación del modelo de convertidor de potencia: Resultados 
A.1. Carga tipo corriente y tensión de entrada alternada
A.2. Carga tipo resistencia y tensión de entrada alternada 
A.3. Carga tipo potencia y tensión de entrada alternada 
A.4. Carga tipo corriente y tensión de entrada fluctuante 

Bibliografía