Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

Imagina que estás construyendo un castillo masivo e intrincado hecho de piezas de Lego digitales. Esto es lo que hacen los ingenieros cuando diseñan chips informáticos: escriben código llamado RTL (Nivel de Transferencia de Registros) que les dice a los diminutos transistores cómo comportarse. Pero aquí está el truco: si incluso un ladrillo se coloca en el lugar equivocado, todo el castillo podría colapsar cuando se encienda la energía. Comprobar estos errores es la parte más difícil del trabajo, y a menudo consume más de la mitad del tiempo. Tradicionalmente, los ingenieros han utilizado dos formas principales para comprobar su trabajo. La primera es como una "prueba de conducción", donde ejecutan el chip a través de algunos escenarios específicos para ver si falla. La segunda es la "verificación formal", que es como una prueba matemática súper compleja que garantiza que el castillo resistirá bajo todas las condiciones posibles, no solo las que probaron. Sin embargo, este método de súper-prueba suele requerir software costoso y cerrado que solo las grandes empresas pueden permitirse.

Entra en escena el nuevo integrante del grupo: los Modelos de Lenguaje Extensos (LLM). Quizás los conozcas como los chatbots de IA que pueden escribir historias o código. Recientemente, la gente empezó a preguntarse: "¿Puede una IA ser el arquitecto que repare nuestros castillos digitales rotos?". La gran pregunta es si una IA puede no solo detectar un error, sino también arreglarlo de una manera que esté matemáticamente probada como perfecta, sin necesidad de comprar una licencia de software de un millón de dólares. Este artículo profundiza en esa pregunta, intentando construir un puente entre la creatividad de la IA y la lógica estricta e inquebrantable de las matemáticas formales, utilizando únicamente herramientas gratuitas y de código abierto.

El detective de IA y la caja de herramientas de código abierto

En este estudio, un investigador llamado Ha Trung Tran construyó un ingenioso equipo de agentes de IA para actuar como una cuadrilla de reparación para diseños de chips rotos. Piensa en ello como un escuadrón de detectives de alta tecnología trabajando en un bucle. En lugar de que un solo agente de IA intente hacerlo todo a la vez, el equipo está dividido: un agente lee los planos, otro escribe las reglas de lo que el chip debería hacer, un tercero comprueba el trabajo y un cuarto realmente arregla el código.

El ingrediente secreto aquí es cómo comprueban los errores. La mayoría de las herramientas de reparación de IA simplemente realizan algunas pruebas de conducción (simulaciones) para ver si el chip funciona. Pero este equipo utiliza un "backend formal": un motor matemático gratuito y de código abierto compuesto por herramientas llamadas Yosys, SymbiYosys y Z3. Este motor no solo adivina; intenta demostrar matemáticamente que el chip es correcto. Si el chip falla, el motor no solo dice "está roto". Entrega a la IA un "contraejemplo" específico, que es como una repetición de video que muestra exactamente cómo colapsó el castillo. La IA observa entonces este video, averigua qué salió mal e intenta arreglarlo. Siguen haciendo esto —comprobar, encontrar el fallo, arreglar, comprobar de nuevo— hasta que las matemáticas demuestran que el chip es perfecto o se quedan sin intentos.

Las buenas noticias: Funciona (a veces)

Los investigadores probaron este sistema en seis tipos diferentes de diseños digitales, que van desde una parte de calculadora simple (una ALU) hasta controladores de tráfico y unidades de memoria más complejos. Los resultados fueron una mezcla de triunfo y limitaciones claras.

La estrella del espectáculo fue la ALU (Unidad Aritmético Lógica), que es como el cerebro de calculadora de un chip. Los investigadores la rompieron intencionadamente intercambiando una operación "AND" por una operación "OR". El equipo de IA detectó el error inmediatamente. En solo dos rondas de comprobación y reparación, repararon el código. Más importante aún, el motor matemático de código abierto demostró con un 100 % de certeza que la solución era correcta para cada número posible que el chip pudiera procesar. Esto ocurrió en las cinco ejecuciones de prueba, tomando un promedio de solo 16,5 segundos. Demostró que la idea funciona: una IA, guiada por herramientas matemáticas de código abierto, puede encontrar y arreglar un error real con una garantía matemática.

Las malas noticias: Donde la IA se quedó atascada

Sin embargo, la historia no es una victoria total. Cuando los investigadores intentaron el mismo proceso en los otros cinco diseños, el equipo de IA chocó contra un muro. No pudieron arreglarlos de forma fiable. El artículo desglosa cuidadosamente por qué fallaron, identificando cuatro "modos de fallo" distintos que actúan como trampas para la IA:

1. La trampa de "demasiado profundo" (Vacuidad de cobertura acotada): En un caso (un contador), el motor matemático dijo "FALLO" a pesar de que la solución era en realidad correcta. ¿Por qué? Porque el diseño necesitaba ejecutarse durante 256 ciclos para alcanzar un estado específico, pero la herramienta solo miró 256 ciclos de profundidad. Era como intentar demostrar que un coche puede cruzar el país conduciendo solo un kilómetro; la herramienta no pudo ver el destino, así que se rindió. El artículo señala que esto es un límite de la herramienta, no de la IA.
2. La trampa de "instrucciones confusas" (Ambigüedad de especificación): Para otro diseño (un árbitro), la IA intentó seguir las reglas escritas, pero las reglas pedían algo imposible (como un semáforo que cambia sin un reloj). La IA siguió fielmente las instrucciones imposibles, lo que la llevó a un callejón sin salida.
3. La trampa del "viaje en el tiempo" (Errores de lógica temporal): En dos casos (un transmisor UART y una memoria FIFO), los errores implicaban eventos que ocurrían a lo largo de múltiples pasos de tiempo. La IA era excelente arreglando la lógica de un solo paso (como la de la calculadora), pero le costaba razonar sobre secuencias de eventos que ocurrían a lo largo del tiempo.
4. La trampa de "demasiadas reglas" (Presión de múltiples propiedades): En el último caso (un esclavo AXI Lite), había tantas reglas que el chip debía seguir simultáneamente que arreglar una regla rompía otra. La IA se quedó atrapada en un bucle, incapaz de encontrar una solución que satisficiera a todos.

Un fallo oculto en la caja de herramientas

También hubo un descubrimiento sorprendente sobre las propias herramientas de código abierto. Los investigadores descubrieron que la herramienta Yosys, que ayuda a procesar el código, tiene una peculiaridad oculta. Si intentas adjuntar las comprobaciones de seguridad (aserciones) al diseño utilizando un método específico llamado "bind", la herramienta las ignora silenciosamente. Es como poner una cámara de seguridad en una habitación pero tener la cámara desenchufada; el sistema cree que todo está bien porque nunca ve la cámara. Los investigadores tuvieron que cambiar su método para "inyectar" las comprobaciones directamente en el código para asegurarse de que el motor matemático realmente las viera. Este es un consejo útil para cualquiera que utilice estas herramientas gratuitas.

La conclusión

Este artículo es un "estudio de viabilidad", que es una forma elegante de decir: "Lo hemos intentado y aquí explicamos exactamente dónde funciona y dónde falla". El hallazgo principal es que es posible utilizar una IA para arreglar diseños de chips con una prueba matemática de corrección, pero solo si se utilizan herramientas de código abierto y si el problema no es demasiado complejo.

El autor es honesto sobre los límites: el sistema es excelente para arreglar errores de lógica simples e inmediatos (como la de la calculadora), pero actualmente tiene dificultades con problemas de tiempo complejos, estados de memoria profundos o diseños con reglas contradictorias. No pretendieron haber resuelto el problema de la reparación de chips; en su lugar, trazaron un mapa claro que muestra la "zona segura" donde la IA funciona y la "zona de peligro" donde se pierde. Al utilizar únicamente herramientas gratuitas, esperan reducir el coste de entrada para este tipo de investigación, demostiendo que no se necesita un presupuesto de un millón de dólares para empezar a construir el futuro del diseño de hardware fiable.