FormalRTL: Verified RTL Synthesis at Scale

El artículo presenta FormalRTL, un marco de trabajo multiagente que integra modelos de referencia de software como especificaciones formales para generar y verificar código RTL de manera escalable y fiable, abordando así los desafíos de los diseños industriales a gran escala mediante la síntesis asistida por modelos de lenguaje grandes.

Lo esencial

Imagina que construir un chip de computadora (como los que tienen los teléfonos o las tarjetas gráficas) es como construir un rascacielos gigante.

Hasta ahora, los ingenieros tenían que dibujar cada ladrillo, cada tubería y cada cable a mano, siguiendo instrucciones escritas en un lenguaje muy técnico y confuso. Era lento, costoso y a veces, si te equivocabas en un solo cable, todo el edificio se caía.

Recientemente, aparecieron los Inteligencias Artificiales (IA) que pueden escribir código. La idea era: "¡Genial! Le pedimos a la IA que escriba los planos del chip y listo". Pero hubo un problema: las IAs a menudo inventaban cosas que no funcionaban, o seguían instrucciones vagas y construían un edificio que se veía bien por fuera pero que se derrumbaba por dentro.

Aquí es donde entra FormalRTL, el nuevo sistema presentado en este paper. Vamos a explicarlo con una analogía sencilla:

El Problema: El Arquitecto que sueña despierto

Antes, le decías a la IA: "Haz un chip que sume números rápido".
La IA intentaba adivinar cómo hacerlo. A veces acertaba, pero a menudo fallaba porque no entendía las reglas ocultas de la física y la electricidad. Era como pedirle a un niño que construya un puente de Lego sin darle las instrucciones del manual; el puente se veía bonito, pero si le ponías un coche encima, se rompía.

La Solución: FormalRTL (El Supervisor con Manual de Instrucciones)

FormalRTL no le pide a la IA que "adivine". En su lugar, le da una receta de cocina perfecta (un modelo de software en C/C++) que ya sabe exactamente cómo debe funcionar el chip.

El sistema funciona como un equipo de construcción de 3 personas muy especializadas:

1. El Planificador (El Jefe de Obra):
   En lugar de darle a la IA todo el edificio de golpe, el Planificador toma la "receta perfecta" y la divide en tareas pequeñas.

   • Analogía: Imagina que tienes que construir una casa. El Planificador no le dice al albañil "construye la casa". Le dice: "Primero, cava los cimientos. Luego, levanta la pared del norte. Luego, pon el techo". Divide el trabajo gigante en trocitos manejables.

2. El Constructor (El Albañil IA):
   Esta es la Inteligencia Artificial. Toma la tarea pequeña (ej. "haz la pared del norte") y la "receta perfecta" correspondiente, y escribe el código (los planos de Lego).

   • La magia: Como tiene la receta exacta, no tiene que inventar nada. Solo tiene que traducir la receta al lenguaje de construcción.

3. El Inspector (El Detective de Errores):
   Aquí está la parte más importante. En lugar de esperar a que la casa esté terminada para ver si se cae, el Inspector revisa cada pared nada más se pone.

   • Usa una herramienta matemática (llamada "verificación formal") que es como un simulador de gravedad perfecto. Compara la pared que construyó la IA con la "receta perfecta".
   • Si la IA puso un ladrillo en el lugar equivocado, el Inspector no dice simplemente "fallaste". Le entrega un reporte detallado que dice: "Oye, en la línea 56, pusiste un ladrillo rojo donde debería ir uno azul. Aquí tienes la foto del error".
   • La IA corrige el error inmediatamente y vuelve a intentar.

¿Por qué es un gran avance?

• No es adivinanza, es certeza: Antes, las IAs hacían cosas que funcionaban "a veces". FormalRTL asegura que el chip funcione siempre, porque lo compara matemáticamente con la receta perfecta.
• Escalable: Puede construir cosas muy grandes (como los chips de las nuevas IAs) porque divide el trabajo en pedazos pequeños. Es como construir un rascacielos: no puedes hacerlo todo de una vez, pero si construyes piso por piso y verificas cada uno, al final tendrás un edificio seguro.
• Ahorra tiempo: Los ingenieros humanos ya no tienen que pasar meses buscando un cable suelto en un código de 10,000 líneas. La IA lo encuentra y lo arregla sola en segundos.

En resumen

FormalRTL es como tener un arquitecto IA que no solo dibuja los planos, sino que tiene un supervisor matemático que revisa cada línea de código contra un manual de instrucciones infalible antes de que se construya nada.

El resultado: Chips más rápidos, más seguros y creados en una fracción del tiempo que tardan los humanos, sin el miedo a que el edificio se derrumbe por un error de cálculo. Es el paso de "construir a ciegas" a "construir con un mapa perfecto".

Resumen técnico

Resumen Técnico: FormalRTL - Síntesis RTL Verificada a Escala

1. Planteamiento del Problema

El diseño de chips computacionales intensivos (como GPUs, NPUs y TPUs) se ha convertido en un cuello de botella debido a la complejidad de su lógica y la búsqueda de metas extremas en potencia, rendimiento y área (PPA). Aunque los Modelos de Lenguaje Grandes (LLMs) han mostrado potencial para automatizar la síntesis de hardware, existen barreras significativas para su aplicación a escala industrial, especialmente en diseños centrados en rutas de datos (datapaths):

• Complejidad de Diseño a Gran Escala: Los núcleos de IP industriales requieren miles de líneas de código RTL. Los enfoques actuales basados en planificación fallan debido a especificaciones en lenguaje natural ambiguas y la dificultad de los LLMs para tomar decisiones arquitectónicas sólidas en diseños complejos.
• Estructuras Aritméticas y Lógicas Intrincadas: A diferencia de los benchmarks de código abierto simples, los IPs industriales tienen rutas de datos anidadas y tipos de datos personalizados (ej. bfloat16, hifloat8). La verificación basada en simulación a menudo falla en cubrir casos límite (corner cases).
• Falta de Garantías Formales: La síntesis directa de RTL desde lenguaje natural carece de garantías de corrección formal. En la industria, los ingenieros dependen de modelos de referencia en software (C/C++) como especificaciones "doradas" (golden specifications) para la verificación de equivalencia formal, un recurso que los métodos anteriores de LLMs han ignorado.

2. Metodología: FormalRTL

El artículo presenta FormalRTL, un marco de trabajo novedoso de agentes múltiples que integra modelos de referencia de software como especificaciones formales ejecutables para guiar la generación y verificación de código RTL. El flujo de trabajo se divide en tres agentes principales:

1. Agente de Planificación (Planning Agent):

   • Realiza un análisis estático sobre el modelo de referencia en C (utilizando el AST del compilador Clang) para descomponer el diseño complejo en subtareas modulares.
   • Refactoriza la especificación general en especificaciones dirigidas para cada submódulo basándose en las dependencias funcionales del C.
   • Genera los submódulos siguiendo un orden topológico de dependencias, permitiendo una verificación de abajo hacia arriba (bottom-up).

2. Agente de Inicialización (Initializing Agent):

   • Genera el código RTL inicial y un harness de verificación (entorno de prueba) anclado al modelo de referencia.
   • Establece un entorno donde se asumen entradas idénticas y se asserta la equivalencia de salidas entre el código C y el RTL.
   • Determina el marco temporal (número de ciclos de reloj) necesario para la lógica secuencial, alineando las etapas de la tubería (pipelining) con los requisitos de latencia.

3. Agente de Depuración (Debugging Agent):

   • Utiliza herramientas de Verificación de Equivalencia Formal (EC) (específicamente hw-cbmc) para comparar el modelo de software y el hardware.
   • Recibe dos tipos de retroalimentación:
     • Errores de sintaxis: Un localizador de errores identifica la línea y extrae el contexto para facilitar la corrección al LLM.
     • Contrajejemplos (Counterexamples): Un simplificador reduce el informe de error para mostrar solo las señales y funciones conflictivas.
   • El LLM utiliza esta información para generar parches de código automáticamente, cerrando el ciclo de depuración sin necesidad de crear testbenches manuales.

3. Contribuciones Clave

• Metodología Guiada por Modelos de Referencia: Pionera en el uso de modelos de software (C/C++) como especificaciones formales ejecutables para guiar la síntesis de hardware ágil, asegurando escalabilidad y corrección.
• Motor Multi-Agente End-to-End: Desarrollo de un sistema automatizado que orquesta la planificación, síntesis, depuración y verificación formal en un solo flujo integrado.
• Nueva Suite de Benchmarks Industriales: Creación y liberación de un conjunto de benchmarks de grado industrial (incluyendo operadores FP16 y tipos de datos hifloat8 para chips Ascend) que incluyen especificaciones detalladas y modelos de referencia en C, llenando un vacío en la investigación actual.
• Código de Fuente Abierto: Promesa de liberar el framework FormalRTL y la suite de benchmarks para fomentar la investigación futura.

4. Resultados Experimentales

Los experimentos se realizaron en una suite de benchmarks académicos y industriales, utilizando LLMs como GPT-4.1 y GPT-5.

• Eficacia en Complejidad Industrial: El sistema logró generar y verificar diseños con más de 1000 líneas de código RTL.
• Tasa de Éxito Final (FSR):
  • Los submódulos alcanzaron una FSR alta (entre 80% y 100%) dentro de los límites de iteración, demostrando la eficacia de la depuración guiada por contrajejemplos.
  • En diseños secuenciales complejos, el sistema mantuvo una alta tasa de éxito, superando las dificultades inherentes a la lógica secuencial.
• Estudio de Ablación (Planificación):
  • Comparado con un enfoque de línea base que solo usa especificaciones en lenguaje natural (sin análisis estático de C), FormalRTL mostró una estabilidad y escalabilidad superiores.
  • A medida que aumentaba la complejidad del diseño, el método de línea base falló (0% de éxito en el diseño más complejo), mientras que FormalRTL mantuvo altas tasas de éxito gracias a la descomposición modular.
• Estudio de Ablación (Depuración):
  • La ausencia de la guía por contrajejemplos causó la mayor degradación de rendimiento (FSR del 55% vs 95% con el sistema completo), confirmando que la retroalimentación formal es crítica.
• Calidad del Resultado (QoR):
  • Los diseños generados por LLM mostraron un área y retraso ligeramente superiores a los diseños manuales optimizados por ingenieros. Sin embargo, el artículo enfatiza que la corrección funcional es el primer paso, y un RTL verificado proporciona una base sólida para iteraciones posteriores de optimización PPA.

5. Significado e Impacto

El trabajo FormalRTL representa un avance crucial al cerrar la brecha entre los prototipos de investigación basados en LLM y el desarrollo de hardware industrial real.

• Cambio de Paradigma: Transita de la síntesis basada puramente en lenguaje natural a un enfoque híbrido que aprovecha la precisión de los modelos de software existentes.
• Garantías Formales: Introduce garantías de corrección matemática en la generación de hardware automatizado, algo que antes era inexistente en los enfoques de LLM.
• Escalabilidad: Demuestra que es posible manejar diseños industriales complejos mediante la descomposición inteligente y la verificación incremental, ofreciendo una ruta viable hacia la automatización de la síntesis de chips de próxima generación.

En conclusión, FormalRTL no solo genera código, sino que genera código verificado, estableciendo un nuevo estándar para la síntesis de hardware asistida por IA.