Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

Este artículo presenta una metodología escalable para la verificación formal de la aritmética de punto flotante que, mediante un enfoque modular de comprobación de modelos RTL-a-RTL, estrategias de refinamiento guiadas por contraejemplos y la integración de inteligencia artificial generativa con supervisión humana, logra una mayor eficiencia de cobertura y reduce la dependencia de modelos de alto nivel.

Lo esencial

Imagina que estás construyendo un reloj de precisión milimétrica (el hardware) y necesitas asegurarte de que funciona exactamente igual que el dibujo original del arquitecto (el modelo de referencia). Si el reloj se atrasa un segundo o marca la hora incorrecta, podría causar problemas graves, especialmente si ese reloj controla un avión o un sistema médico.

Este artículo trata sobre cómo verificar que los "relojes" matemáticos de las computadoras (llamados Unidades de Punto Flotante, que hacen cálculos con decimales) funcionen perfectamente, sin errores.

Aquí tienes la explicación sencilla, paso a paso:

1. El Problema: Traducir idiomas extraños

Antes, para verificar estos diseños, los ingenieros hacían algo como traducir el plano del reloj (código de hardware) a un idioma de alto nivel (como C o un modelo matemático abstracto) para compararlo.

• La analogía: Es como intentar verificar si un coche de carreras es rápido traduciendo sus planos técnicos a un poema. El poema puede sonar bonito, pero pierde detalles cruciales sobre los tornillos y el motor. Además, el proceso de traducción es lento y a veces introduce errores nuevos.

2. La Solución Propuesta: Comparación Directa "Ojo a Ojo"

Los autores proponen una nueva forma: no traducir nada. Comparan directamente el diseño final (el código de hardware) contra el modelo perfecto (el "estándar de oro").

• La analogía: En lugar de traducir el plano a un poema, pones el coche de carreras al lado del coche de competición perfecto y los comparas pieza por pieza, tornillo por tornillo, directamente. Es más rápido y no hay riesgo de que la traducción oculte un error.

3. La Estrategia: Desarmar para entender (Divide y Vencerás)

Verificar todo el reloj de golpe es imposible porque hay demasiadas piezas. Ellos descomponen el problema en etapas pequeñas.

• La analogía: Imagina que tienes que verificar una receta de cocina gigante. En lugar de probar todo el plato al final, verificas paso a paso:
  1. ¿Se cortaron bien las verduras? (Etapa de alineación).
  2. ¿Se cocinaron bien y se sazonaron? (Etapa de suma y redondeo).
     Si algo sale mal en la etapa 1, no tienes que esperar a que se queme todo el plato para saberlo. Corriges ese paso y sigues.

4. El Nuevo Héroe: La Inteligencia Artificial (IA) como Ayudante

Aquí es donde entra la parte más moderna del artículo. Usaron una IA con "agentes" (un equipo de robots virtuales) para escribir las reglas de verificación.

• La analogía: Imagina que tienes un chef novato (la IA) que quiere escribir las reglas de la receta.
  • Al principio, el chef escribe muchas reglas, algunas repetidas o confusas (como decir "corta la cebolla" y luego "corta la cebolla en trozos" por separado).
  • Aquí entra el Chef Jefe Humano (Human-in-the-Loop). El humano revisa lo que escribió la IA, le dice: "Oye, esa regla sobra, y esta otra necesita ser más precisa".
  • Resultado: Con la ayuda del humano, la IA aprende a escribir reglas perfectas, rápidas y sin redundancias.

5. Los Resultados: ¿Funcionó?

• Sin IA: Los ingenieros expertos escribieron las reglas a mano. Fue muy rápido y preciso.
• IA sola: La IA escribió muchas reglas, pero algunas eran redundantes (repetitivas) y tardaba más en verificar.
• IA + Humano: Esta fue la combinación ganadora. La IA generó las ideas, el humano las pulió. El resultado fue casi tan bueno como el experto humano, pero mucho más rápido de producir.

6. La Prueba de Fuego: Inyectar Errores

Para asegurarse de que su método era bueno, los autores hicieron algo arriesgado: introdujeron errores a propósito en el diseño (como cambiar un signo o mover un número).

• La analogía: Es como si un inspector de seguridad metiera una bomba falsa en el coche para ver si el sistema de alarma la detecta.
• Resultado: ¡Funcionó! El sistema detectó todos los errores que ellos mismos habían creado. Esto demuestra que el método es robusto y no se deja engañar por fallos sutiles.

En Resumen

Este paper nos dice que para verificar que los cálculos matemáticos de las computadoras sean perfectos:

1. No hay que traducir el código a otros lenguajes; hay que compararlo directamente.
2. Hay que dividir el problema en trozos pequeños.
3. La Inteligencia Artificial puede ayudar a escribir las reglas de verificación, pero necesita la guía de un humano experto para ser realmente eficiente y evitar redundancias.

Es una mezcla de matemáticas estrictas (para garantizar que no haya errores) con inteligencia artificial moderna (para acelerar el proceso), todo supervisado por ingenieros humanos que aseguran que la IA no se pierda en el camino.

Resumen técnico

Resumen Técnico: Verificación Formal de Aritmética de Punto Flotante

1. Planteamiento del Problema

La verificación formal de unidades de punto flotante (FPU) representa uno de los desafíos más complejos en el diseño de hardware debido a:

• Comportamiento no lineal: La interacción entre la lógica de control discreta y las rutas de datos aritméticas crea un espacio de estados difícil de explorar.
• Requisitos estrictos: El cumplimiento de la norma IEEE-754 introduce casos borde complejos (desnormalizados, desbordamiento, subdesbordamiento, pérdida de precisión).
• Limitaciones de los enfoques actuales: La mayoría de las metodologías existentes dependen de modelos de alto nivel en C para la verificación de equivalencia contra el diseño a nivel de Registro a Transistor (RTL). Esto introduce:
  • Brechas de abstracción entre el modelo C y la implementación de hardware.
  • Sobrecarga de traducción y mantenimiento.
  • Problemas de escalabilidad al aplicar verificación directa a nivel de RTL.

2. Metodología Propuesta

El artículo presenta una metodología escalable que evita los modelos de software, basándose en la verificación directa RTL-a-RTL mediante model checking. Los pilares de la metodología son:

• Model Checking Directo RTL-a-RTL: Se compara una implementación RTL (diseño bajo verificación) contra un modelo de referencia "golden" también en RTL (SystemVerilog), eliminando la necesidad de modelos C.
• Estrategia de Dividir y Conquistar (Descomposición Jerárquica):
  • El diseño se descompone en etapas modulares para reducir el cono de influencia (COI) y la complejidad de la prueba.
  • Se utiliza un teorema principal de corrección respaldado por lemas intermedios.
  • Caso de Estudio: Un sumador de punto flotante descompuesto en dos etapas:
    1. Alineación de Mantisa: Ajuste de exponentes y alineación de mantisas.
    2. Suma y Redondeo: Adición, normalización y redondeo final.
• Refinamiento Guiado por Contraejemplos (CEX): Si la herramienta formal encuentra una discrepancia, genera un contraejemplo (CEX) que permite aislar y corregir defectos en la implementación o refinar las propiedades.
• Generación de Propiedades con IA Agente: Se implementó un sistema multi-agente (Lead Agent, Critic Agent, Error Correction Agent) que utiliza Modelos de Lenguaje Grande (LLM) para generar propiedades en SystemVerilog (SVA) a partir de especificaciones naturales, con un ciclo de Human-in-the-Loop (HITL) para refinar y validar las propiedades.

3. Contribuciones Clave

1. Verificación RTL-a-RTL sin abstracción C: Demuestra la viabilidad de verificar la equivalencia funcional directamente en el nivel de hardware, garantizando una precisión bit a bit sin brechas semánticas.
2. Prueba Estructurada por Lemas: Establece un marco donde la corrección global se prueba mediante la validación de lemas específicos para cada etapa modular (Alineación y Suma/Redondeo).
3. Inyección de Fallos: Se validó la robustez del proceso mediante la inyección sistemática de fallos en la ruta de datos (ej. errores en bits "sticky", alineación incorrecta, reglas de redondeo) para asegurar que las propiedades formales detectan errores críticos de precisión.
4. Análisis de Cobertura con IA: Comparación exhaustiva entre propiedades escritas a mano y propiedades generadas por IA (GPT-5, Llama3.3, GPT-4o) en dos escenarios: con modelo de referencia y verificación RTL independiente.

4. Resultados y Evaluación

Los experimentos se realizaron utilizando la plataforma Cadence Jasper Formal Verification.

• Detección y Corrección de Errores: La metodología identificó y corrigió fallos reales en el sumador de punto flotante de código abierto, como selección incorrecta de operandos cuando los exponentes eran iguales y lógica de inversión defectuosa durante la resta.
• Eficiencia de Cobertura (RTL-a-RTL con Referencia):
  • Las propiedades escritas a mano lograron un 98.42% de cobertura formal con solo 2 aserciones y un tiempo de prueba de 0.073s.
  • Las propiedades generadas por IA inicialmente requirieron más aserciones (7-15) y tiempos mayores debido a redundancias. Sin embargo, tras el refinamiento HITL, los modelos de IA (especialmente GPT-5) lograron eficiencias comparables, reduciendo el conjunto a 3-6 aserciones válidas sin contraejemplos.
• Verificación RTL Independiente (Sin Referencia):
  • Sin un modelo de referencia, la cobertura cayó significativamente (ej. ~62% para Llama3.3 sin HITL) debido a la falta de restricciones arquitectónicas.
  • Se requirió un esfuerzo sustancial de HITL para añadir restricciones micro-arquitectónicas específicas (propagación de bits sticky, profundidad de normalización) para alcanzar coberturas superiores al 90% (GPT-5 con HITL alcanzó 92.30%).
• Robustez: La inyección de 8 fallos distintos (4 en alineación, 4 en suma/redondeo) fue detectada exitosamente por todas las propiedades formales, confirmando la sensibilidad del método.

5. Significado e Impacto

Este trabajo es significativo porque:

• Elimina la dependencia de modelos C: Proporciona un flujo de verificación más preciso y escalable para diseños de datapath complejos, evitando errores de traducción.
• Valida el uso de IA en Verificación Formal: Demuestra que los LLMs pueden generar propiedades formales útiles, pero el ciclo de retroalimentación humana (HITL) es crítico para eliminar redundancias, corregir suposiciones inválidas y alinear las propiedades con la intención micro-arquitectónica.
• Establece un nuevo estándar: La combinación de descomposición jerárquica, verificación RTL-a-RTL y generación asistida por IA ofrece una estrategia más eficiente que la verificación formal independiente para unidades aritméticas complejas.

En conclusión, el artículo propone un marco robusto para la verificación de FPU que combina la rigurosidad matemática de la verificación formal directa con la automatización emergente de la IA, reduciendo el esfuerzo humano mientras mantiene altos niveles de cobertura y corrección.