💬 NLP

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

CktFormalizer es un marco que aprovecha el HDL con tipos dependientes de Lean 4 para guiar a los LLM en la generación de descripciones de hardware que están garantizadas como sintácticamente correctas, libres de defectos que rompan la síntesis y verificadas funcionalmente mediante pruebas comprobadas por máquina, logrando así una realizabilidad casi perfecta en la etapa posterior y habilitando una optimización segura y automatizada del PPA.

Autores originales: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Publicado 2026-05-11

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que le pides a un arquitecto muy talentoso pero ligeramente descuidado que dibuje un plano para una casa basado en una descripción verbal.

En el mundo tradicional del diseño de chips, le pedirías al arquitecto que escriba las instrucciones en Verilog (un lenguaje utilizado para describir chips informáticos). El arquitecto podría escribir una descripción hermosa, pero como Verilog es un poco como un conjunto de reglas laxas, el arquitecto podría decir accidentalmente: "Conecta una tubería de 4 pulgadas con una de 8 pulgadas", o "Crea un pasillo que regresa a sí mismo".

La computadora verifica la gramática y dice: "¡Parece bien!". Pero cuando la casa se construye realmente (cuando el chip se fabrica), esos errores hacen que las tuberías estallen o que el pasillo atrape a las personas. Estos son fallos costosos y silenciosos que solo aparecen semanas después.

CKTFORMALIZER es un nuevo marco que cambia el juego. En lugar de permitir que el arquitecto escriba directamente en el lenguaje laxo de Verilog, lo obliga a escribir en un lenguaje estricto y matemático llamado Lean.

Así es como funciona, usando una analogía simple:

1. El Editor Estricto (El Compilador)

Piensa en Lean como un editor súper estricto que sabe exactamente cómo debe construirse una casa.

La Vieja Forma: El arquitecto escribe "Conecta la tubería A con la tubería B". El editor no verifica los tamaños. Más tarde, el equipo de construcción descubre que la tubería A es demasiado pequeña.
La Forma CKTFORMALIZER: El arquitecto intenta escribir "Conecta la Tubería A (tamaño 4) con la Tubería B (tamaño 8)". El editor cierra de golpe la puerta y dice: "¡Error! No puedes conectar estas. Arréglalo ahora."
El Resultado: El arquitecto (una IA) recibe retroalimentación instantánea. No puede avanzar hasta que los tamaños coincidan perfectamente. Esto detecta "desajustes de ancho" y "bucles" antes de que se coloque un solo ladrillo.

2. La Red de Seguridad (Seguridad de Tipos)

En el sistema antiguo, podrías dejar accidentalmente una puerta abierta en una habitación, y la casa se construiría con una habitación con corrientes de aire y rota. En el sistema Lean, las reglas son tan estrictas que es físicamente imposible escribir un plano con una habitación rota.

Si el arquitecto olvida describir qué sucede cuando se acciona un interruptor, el editor dice: "¡Te has saltado un caso! Debes describir cada posibilidad".
Esto asegura que el diseño sea "correcto por construcción". Si se compila (pasa la verificación del editor), está garantizado que sea estructuralmente sólido.

3. La Prueba de Verdad (Verificación Formal)

Por lo general, para verificar si un diseño de casa funciona, construyes un modelo pequeño y lo pruebas. A veces el modelo funciona, pero la casa real no.
CKTFORMALIZER utiliza pruebas matemáticas. La IA no solo adivina; escribe una prueba matemática que dice: "Este nuevo diseño, más barato, hace exactamente lo mismo que el diseño original perfecto".

Es como tener un matemático que demuestra que tu nuevo plano, más barato, es 100% idéntico en función al original, hasta el último átomo, para cada escenario posible, no solo para los que probaste.

4. El Bucle de Optimización (El Renovador Inteligente)

Una vez que la IA tiene un diseño que funciona, el sistema no se detiene. Actúa como un renovador inteligente que mira el plano y dice: "Podemos hacer esta casa un 35% más pequeña y usar un 30% menos de energía".

La IA intenta reorganizar las habitaciones (la lógica del circuito).
Construye una nueva versión.
Ejecuta inmediatamente el "Editor Estricto" nuevamente para asegurarse de que la nueva versión funcione perfectamente.
Luego ejecuta una simulación física para ver cuánto espacio y energía ahorra.
Si la nueva versión es mejor y sigue estando matemáticamente probada como correcta, la conserva. Si no, la deshace.

Los Resultados

El artículo probó esto en cientos de problemas de diseño (como construir contadores, unidades de memoria y controladores de semáforos).

La Línea Base (Vieja Forma): Cuando intentaron construir los chips, aproximadamente el 20% de los diseños que parecían correctos en el papel fallaron realmente cuando intentaron fabricarlos.
CKTFORMALIZER (Nueva Forma): El 100% de los diseños que pasaron el editor estricto lograron atravesar todo el proceso de fabricación (síntesis, colocación y enrutamiento) sin fallar.
Eficiencia: El sistema también logró reducir los diseños y ahorrar energía significativamente (hasta un 35% menos de área) mientras demostraba que seguían siendo perfectos.

En Resumen

CKTFORMALIZER es como darle a un arquitecto de IA un libro de reglas mágico que le impide cometer errores antes de empezar a dibujar. En lugar de construir una casa y esperar a que no se derrumbe, obliga al arquitecto a demostrar que la casa es sólida antes de pedir el primer ladrillo. Esto convierte el diseño de chips de un juego de "adivinar y verificar" en un proceso de "demostrar y construir", resultando en chips más pequeños, más eficientes y garantizados para funcionar.

Resumen Técnico: CktFormalizer

Enunciado del Problema

El diseño de hardware sigue siendo una disciplina propensa a errores, donde defectos sutiles, como desajustes de ancho de bits, bucles combinacionales o lógica de casos incompleta en Máquinas de Estado Finito (FSM), pueden pasar las comprobaciones de sintaxis pero fallar silenciosamente durante la síntesis o manifestarse como errores costosos en el silicio más adelante. Aunque los Modelos de Lenguaje Grande (LLM) han demostrado la capacidad de generar Verilog a partir de especificaciones en lenguaje natural, el código resultante a menudo hereda las trampas inherentes de Verilog y VHDL: la falta de garantías estáticas como tipos dependientes, coincidencia de patrones exhaustiva y pruebas verificadas por máquina. En consecuencia, el hardware generado por LLM requiere frecuentemente una depuración manual extensa y a menudo falla al alcanzar la implementación física (Colocación y Enrutamiento, DRC, LVS), incluso cuando es funcionalmente correcto en la simulación.

Metodología

El artículo presenta CktFormalizer, un marco que unifica la generación de código impulsada por LLM con la verificación formal al dirigirse a un Lenguaje de Descripción de Hardware (HDL) con tipos dependientes incrustado en Lean 4. En lugar de generar Verilog directamente, el sistema redirige al agente LLM para que genere código Lean, el cual sirve como el objetivo principal de compilación.

Arquitectura Central

El marco opera a través de un pipeline de bucle cerrado que involucra tres roles distintos para Lean:

Verificador de Tipos (Verificador en Tiempo de Compilación): El sistema de tipos dependiente de Lean codifica restricciones de ancho de bits, cobertura de casos y aciclicidad. Los defectos de hardware (por ejemplo, desajustes de ancho o bucles combinacionales) se detectan como errores de tipo en tiempo de compilación en lugar de fallos silenciosos en el backend. Esto proporciona al agente LLM una retroalimentación inmediata y accionable para reparar iterativamente el diseño.
Cortafuegos de Corrección: Los diseños que se compilan con éxito en Lean están estructuralmente garantizados para estar libres de clases específicas de defectos (desajustes de ancho, bucles combinacionales, cierres no deseados). Esto asegura que los diseños compilados sobrevivan al flujo de síntesis y Colocación y Enrutamiento (P&R) del backend sin la tasa de pérdida del 20% observada en la generación base de Verilog.
Asistente de Pruebas: El agente construye pruebas de teoremas automatizadas para verificar la equivalencia funcional entre la especificación en lenguaje natural y la implementación generada (u optimizada). Estas pruebas cubren secuencias de entrada arbitrarias y anchos parametrizados, yendo más allá de las limitaciones de la verificación basada en SMT acotada.

Flujo de Trabajo

Generación e Iteración: Un agente LLM (instanciado con Claude) genera código HDL en Lean basado en una especificación en lenguaje natural. Entra en un bucle iterativo de "generar-compilar-reparar" donde los errores del compilador de Lean guían al agente para corregir errores semánticos antes de que se propaguen.
Extracción: Tras una compilación exitosa, un metaprograma (#synthesizeVerilog) extrae SystemVerilog sintetizable del grafo de combinadores de señales de Lean.
Implementación Física: El SystemVerilog extraído se simula, se sintetiza (usando Yosys) y se implementa físicamente (usando OpenROAD con el PDK de SkyWater de 130 nm) para generar diseños GDSII y métricas de Potencia-Rendimiento-Área (PPA).
Bucle de Optimización PPA: Una etapa de optimización de bucle cerrado devuelve las métricas PPA al agente. El agente propone variantes arquitectónicas (por ejemplo, rutas de datos paralelas frente a seriales) y debe proporcionar pruebas de equivalencia verificadas por máquina para asegurar que la variante optimizada permanezca funcionalmente equivalente a la especificación original.

Contribuciones Clave

Primer Marco de Extremo a Extremo: CktFormalizer es el primer marco que combina la generación de hardware impulsada por LLM con un HDL incrustado en Lean, proporcionando un pipeline desde el lenguaje natural hasta el silicio sintetizable con optimización de PPA de bucle cerrado.
Generación Guiada por Tipos: El artículo demuestra que dirigirse a un HDL seguro por tipos mejora sustancialmente las tasas de éxito de los LLM en comparación con la generación directa de Verilog. Los errores de tipo en tiempo de compilación proporcionan una retroalimentación estructurada que guía al agente hacia diseños correctos, escalando a IP relevante para la industria como interfaces de bus de handshake multicanal.
Integración de Verificación Formal: El marco cierra la brecha entre el código generado por LLM y el hardware demostrablemente correcto al permitir que el agente produzca pruebas de equivalencia verificadas por máquina. Esto asegura que las optimizaciones arquitectónicas no comprometan la corrección funcional.

Resultados Experimentales

El marco fue evaluado en tres puntos de referencia: VerilogEval (156 problemas), RTLLM (50 problemas) y ResBench (56 problemas).

Realizabilidad en el Backend: Un hallazgo crítico es que CktFormalizer preserva la corrección funcional a través del backend. Mientras que la línea base (generación directa de Verilog) pierde aproximadamente el 20% de los diseños funcionalmente correctos durante la síntesis y el enrutamiento, CktFormalizer preserva el 100% de sus diseños compilados a través del flujo completo de síntesis, P&R, DRC y LVS.
Compilación y Simulación: En VerilogEval, CktFormalizer logró una tasa de compilación de Lean del 92,3% y una tasa de aprobación de simulación RTL del 72,4%, compitiendo con las líneas base de generación directa de Verilog. Cuando se incluye la retroalimentación de síntesis en el bucle del agente, la tasa de compilación aumenta al 99,4%.
Optimización PPA: La etapa de optimización de bucle cerrado produjo mejoras significativas. A través de una exploración de arquitectura validada, el marco logró una reducción de área de hasta 35% y una reducción de potencia del 30%.
Cierre de Temporización: Todos los diseños funcionalmente correctos que completaron la Colocación y Enrutamiento lograron el cierre de temporización (WNS $\ge$ 0 ns) sin intervención manual.
Generación de Pruebas: En un estudio piloto, la generación de pruebas paso a paso (refinamiento iterativo con retroalimentación de objetivos de prueba) mejoró las tasas de finalización de pruebas del 53% al 63%, demostrando la viabilidad de los asistentes de prueba para la verificación de hardware.

Significado y Afirmaciones

El artículo afirma que los tipos dependientes y los agentes LLM son complementarios. Al utilizar un lenguaje formal (Lean) tanto como objetivo de generación como sustrato de verificación, el marco transforma el bucle "generar y probar" del LLM de una búsqueda estocástica sobre programas sintácticamente válidos en un proceso de refinamiento guiado por tipos.

Los autores enfatizan que el compilador actúa como el verificador, desplazando la detección de errores desde el final del pipeline EDA (donde las correcciones son costosas) hacia el tiempo de compilación. Este enfoque permite que el sistema produzca hardware que no solo es funcionalmente correcto, sino también estructuralmente robusto frente a transformaciones del backend, resolviendo efectivamente el problema de "fallo silencioso" común en el hardware generado por LLM. El trabajo sugiere que los lenguajes formales pueden servir como base para un diseño de hardware automatizado y confiable, permitiendo a los LLM navegar los complejos compromisos de la optimización de hardware mientras mantienen garantías rigurosas de corrección.