🤖 AI

NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

Este artículo presenta NeuroAbs, un marco neuro-simbólico que aprovecha los LLM para la identificación de señales RTL y la representación simbólica basada en AST, combinado con la verificación de solidez basada en SMT y el refinamiento CEGAR, para automatizar la abstracción de RTL y acelerar significativamente la verificación de propiedades de hardware.

Autores originales: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

Publicado 2026-08-19

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

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

En el mundo oculto de la electrónica moderna, los chips que impulsan nuestros teléfonos, coches y ordenadores se construyen a partir de miles de millones de diminutos interruptores. Antes de que estos chips lleguen a fabricarse, los ingenieros deben demostrar que se comportarán exactamente como se pretende, sin importar las instrucciones que reciban. Este proceso, conocido como verificación formal, es una rigurosa comprobación matemática que garantiza que un diseño esté libre de fallos ocultos. Sin embargo, a medida que estos diseños se vuelven más complejos, la tarea de comprobarlos se vuelve abrumadora. El enorme número de estados posibles en los que un chip puede entrar es tan vasto que incluso los ordenadores más potentes tienen dificultades para explorarlos todos en un tiempo razonable. Para solucionar esto, los ingenieros suelen utilizar una técnica llamada abstracción, que simplifica un diseño complejo eliminando los detalles que no importan para una prueba específica, de forma muy parecida a mirar el mapa de una ciudad que muestra solo las carreteras principales necesarias para un viaje específico mientras ignora cada calle secundaria y callejón.

Durante años, la creación de estos modelos simplificados requirió o bien un tedioso trabajo manual por parte de expertos humanos, o bien dependió de reglas rígidas y preprogramadas que a menudo pasaban por alto los matices de un diseño específico. Un nuevo enfoque llamado NeuroAbs ofrece un camino diferente, combinando la capacidad de reconocimiento de patrones de la inteligencia artificial con la lógica estricta de la matemática formal. Este método utiliza modelos de lenguaje de gran tamaño —sistemas de IA avanzados entrenados en vastas cantidades de texto— para comprender la intención detrás de un diseño de hardware y una propiedad específica que este debe satisfacer. La IA identifica qué partes del circuito son irrelevantes para la prueba actual y sugiere cómo simplificarlas. Sin embargo, debido a que la IA a veces puede cometer errores o sugerir cambios que rompen la lógica, el sistema no confía ciegamente en la IA. En su lugar, actúa como un marco neuro-simbólico, donde la IA propone cambios y un motor matemático separado y riguroso comprueba inmediatamente si esos cambios son seguros. Si la simplificación es demasiado agresiva y corre el riesgo de ocultar un error real, el sistema refina automáticamente el modelo, despojando las capas de simplificación lo justo para restaurar la precisión sin perder los beneficios de la velocidad.

Los investigadores detrás de NeuroAbs probaron su marco en varios diseños de procesadores del mundo real y componentes periféricos, incluyendo una interfaz de comunicación común utilizada en muchos dispositivos. Descubrieron que el sistema podía identificar con éxito oportunidades para simplificar la lógica que los métodos tradicionales basados en reglas pasaban por alto. Por ejemplo, al verificar una instrucción específica en un procesador, la IA se dio cuenta de que la lógica que gestiona otras instrucciones no relacionadas podía sustituirse de forma segura por un marcador de posición genérico. Esto permitió que el motor de verificación se centrara únicamente en las partes relevantes del circuito. En los experimentos, este enfoque aceleró significamente el tiempo requerido para demostrar que un diseño era correcto. Cuando los investigadores integraron NeuroAbs con herramientas de verificación de alto rendimiento ya existentes, el tiempo necesario para alcanzar una prueba formal disminuyó casi a la mitad en muchos casos. Incluso cuando no era posible alcanzar una prueba completa dentro del límite de tiempo, los modelos simplificados permitieron al sistema explorar mucho más profundamente el comportamiento del circuito, descubriendo posibles errores que de otro modo habrían permanecido ocultos.

El éxito de este método reside en un equilibrio cuidadoso entre la flexibilidad de la IA y la precisión de la lógica formal. El sistema analiza primero el diseño y el escenario de prueba específico para señalar qué señales son críticas. Luego utiliza la IA para reescribir el código en esas áreas específicas, sustituyendo cálculos complejos por valores abstractos más sencillos. Crucialmente, cada reescritura es sometida a una estricta comprobación matemática para asegurar que no altera el comportamiento fundamental del chip de una manera que invalide la prueba. Si la comprobación falla, el sistema utiliza un bucle de retroalimentación para identificar exactamente qué simplificación causó el problema y revierte esa parte específica a su forma original. Este proceso iterativo asegura que el modelo final sea lo suficientemente simple para verificarse rápidamente y lo suficientemente preciso para ser fiable. Los resultados muestran que este enfoque híbrido puede manejar diversos tipos de lógica de hardware, desde operaciones aritméticas simples hasta estructuras de ramificación complejas, convirtiéndolo en una herramienta poderosa para la próxima generación de diseño de chips.

Al automatizar la creación de estos modelos simplificados, NeuroAbs aborda un cuello de botella importante en la ingeniería de hardware. Anteriormente, la decisión de qué simplificar y cómo hacerlo dependía en gran medida de la intuición humana o de reglas fijas que no podían adaptarse a cada desafío de diseño único. Este nuevo marco demuestra que la inteligencia artificial puede ser guiada eficazmente para realizar estas tareas, siempre que esté anclada por un sistema que verifique cada paso. Los hallazgos sugieren que el futuro de la verificación de hardware puede residir en tales sistemas colaborativos, donde las máquinas se encargan del trabajo pesado de reconocimiento de patrones y sugerencias, mientras que el rigor matemático garantiza la seguridad y la corrección del producto final. A medida que los diseños de chips continúan creciendo en complejidad, herramientas como NeuroAbs ofrecen una forma prometedora de mantener el ritmo, asegurando que los dispositivos en los que confiamos estén construidos sobre una base de verdad verificada.

Resumen Técnico: NeuroAbs

Declaración del Problema

La verificación formal, específicamente la comprobación de propiedades (model checking), es esencial para garantizar la corrección funcional de los diseños de hardware. Sin embargo, a medida que los diseños de nivel de transferencia de registros (RTL) crecen en tamaño y complejidad, la comprobación eficiente de las propiedades especificadas por el usuario se convierte en un cuello de botella significativo. Aunque se utilizan técnicas de abstracción para reducir la complejidad del sistema reemplazando modelos concretos con representaciones simplificadas, los métodos existentes enfrentan dos limitaciones primarias:

Abstracción Manual: Depende fuertemente de la visión humana y requiere mucho trabajo, obligando a los ingenieros a identificar manualmente qué partes del diseño son irrelevantes para una propiedad específica.
Abstracción Automática Basada en Reglas: Las técnicas como la abstracción estructural, la abstracción guiada por sintaxis y la abstracción de datapath (por ejemplo, reemplazar aritmética con funciones no interpretadas) carecen de flexibilidad. A menudo no logran identificar oportunidades de abstracción que dependen de la intención semántica específica de un escenario de verificación y de la propiedad objetivo, ya que dependen de reglas sintácticas predefinidas en lugar de una comprensión funcional.

Consecuentemente, los métodos actuales suelen perder oportunidades de abstraer de forma segura la lógica que es irrelevante para un objetivo de verificación específico, o producen abstracciones que son demasiado gruesas (provocando contraejemplos espurios) o demasiado conservadoras (fallando en acelerar la verificación).

Metodología: El Marco de Trabajo NeuroAbs

El artículo propone NeuroAbs, un marco neuro-simbólico que integra Modelos de Lenguaje de Gran Escala (LLMs) con razonamiento simbólico para automatizar la abstracción de RTL. El marco opera en tres etapas distintas:

1. Análisis de Señales Asistido por LLM (Componente Neuronal)

En lugar de alimentar bases de código RTL completas a un LLM, lo cual excede los límites de contexto, NeuroAbs emplea un Analizador de Señales para identificar señales candidatas para la abstracción.

Entrada: Especificaciones del diseño, descripciones de escenarios de verificación y definiciones de señales.
Proceso: Utilizando prompting de Cadena de Pensamiento (CoT) e instrucciones de sistema personalizadas, el LLM analiza el escenario de verificación para identificar "señales relacionadas con el escenario". Determina qué señales controlan la lógica relevante para la propiedad específica y sugiere valores fijos (por ejemplo, establecer un opcode a un tipo de instrucción específico).
Integración de Análisis Estático: La salida del LLM se combina con el análisis estático de RTL (por ejemplo, propagación de constantes) para localizar las regiones de código específicas y las sentencias afectadas por estas señales. Esto reduce el alcance de todo el diseño a un pequeño conjunto de sentencias candidatas.

2. Abstracción Guiada por AST (Núcleo Neuro-Simbólico)

Para asegurar la integridad estructural y evitar que el LLM reescriba la lógica no relacionada, NeuroAbs convierte el RTL en un Árbol de Sintaxis Abstracta (AST).

Localización: El sistema mapea las señales candidatas identificadas a nodos de sentencia específicos del AST y sus contextos estructurales envolventes (por ejemplo, bloques always, sentencias case).
Transformación: Un segundo LLM, el Abstractor, tiene la tarea de reescribir solo los nodos localizados del AST. Utiliza aprendizaje de pocos disparos (few-shot learning, proporcionando ejemplos de sentencias originales vs. abstraídas) para generar abstracciones candidatas.
Restricción: El LLM está restringido para reescribir solo las partes específicas de una sentencia que se consideran irrelevantes para la propiedad (por ejemplo, reemplazar una operación AND con un valor desconocido X si la propiedad solo concierne a operaciones ADD), preservando la lógica relevante.

3. Validación y Refinamiento Simbólico (Componente Simbólico)

Cada abstracción generada es validada rigurosamente para asegurar que sea una sobre-aproximación sólida del diseño original.

Comprobación SMT: El marco utiliza solvers de Satisfacibilidad Modulo Teorías (SMT) (específicamente Z3) para verificar la condición $\forall V, S(V) \implies \hat{S}(V)$ $\forall V, S (V) ⟹ \hat{S} (V)$ . Esto asegura que cada comportamiento permitido por la sentencia abstracta también es permitido por la original.
- Manejo de valores X: Dado que los solvers SMT no soportan nativamente valores desconocidos (X), estos se traducen en variables frescas vinculadas por cuantificadores existenciales ( $\exists Y$ ) para permitir que el solver los trate como elecciones no deterministas.
Bucle CEGAR Personalizado (R-CEGAR): Si el modelo abstracto falla al probar la propiedad y genera un contraejemplo, el sistema verifica si el contraejemplo es espurio.
- Si es espurio, se aplica una técnica de reducción de contraejemplos para generalizar la traza y localizar exactamente qué sentencia abstraída disparó la violación.
- El sistema entonces revierte solo las sentencias inválidas específicas a su forma original, en lugar de descartar toda la abstracción, e itera el proceso.

Contribuciones Clave

Primera Aplicación de LLMs a la Abstracción de RTL: El artículo presenta a NeuroAbs como el primer marco que utiliza LLMs para identificar y generar abstracciones de RTL, yendo más allá de los enfoques estáticos basados en reglas.
Flujo de Trabajo Neuro-Simbólico: Propone un flujo novedoso donde el componente neuronal (LLM) propone candidatos conscientes del escenario, mientras que el componente simbólico (recorrido de AST y SMT) restringe la reescritura a objetivos estructurales precisos y valida la solidez.
Refinamiento Personalizado (R-CEGAR): Los autores introducen un bucle de refinamiento que utiliza la reducción de contraejemplos para identificar y revertir eficientemente solo las sentencias abstractas específicas que causan contraejemplos espurios, minimizando el número de iteraciones requeridas.

Resultados Experimentales

El marco fue evaluado en un conjunto de benchmarks que incluyen núcleos de procesadores RISC-V (PicoRV32, Piccolo, Flute) y un periférico I2C, cubriendo 55 escenarios de verificación. Los resultados se compararon con model checkers de vanguardia (AVR y RIC3) que ya incluyen mecanismos de abstracción avanzados.

Aceleración de la Prueba Formal: Al integrarse con AVR, NeuroAbs redujo el tiempo de ejecución promedio para la construcción de pruebas formales en un 44.89%. Incluso con las capacidades de abstracción existentes de AVR, NeuroAbs proporcionó mejoras significativas adicionales.
Eficiencia en la Detección de Errores (BMC): Para los casos donde las pruebas formales no pudieron completarse dentro del límite de tiempo, NeuroAbs aceleró significativamente el proceso de Bounded Model Checking (BMC).
- En el caso "Piccolo", la profundidad media de despliegue aumentó de 109.36 a 125.36 ciclos.
- En el caso "Flute", el tiempo requerido para alcanzar la profundidad máxima de la línea base se redujo en un 75.98%.
Estudios de Ablación: Los experimentos confirmaron que tanto el aprendizaje de pocos disparos (few-shot learning) como las instrucciones personalizadas son críticos. Eliminar el aprendizaje de pocos disparos redujo la tasa de sobre-aproximación del 95.27% al 83.51%. Eliminar las instrucciones personalizadas provocó una caída del 98.38% en las sobre-aproximaciones "estrictas" (lo que significa que el modelo tendía a reproducir las sentencias originales en lugar de abstraerlas).
Reducción de Complejidad: El análisis de los circuitos And-Inverter-Gate (AIG) resultantes mostró una reducción sustancial en el índice máximo de variables, confirmando que NeuroAbs simplifica efectivamente la estructura del circuito.

Significado y Reivindicaciones

El artículo afirma que NeuroAbs aborda la rigidez de la abstracción tradicional basada en reglas y la intensidad de trabajo de los métodos manuales. Al combinar las capacidades de razonamiento semántico de los LLM con el rigor de la verificación simbólica, NeuroAbs puede identificar oportunidades de abstracción específicas del contexto que las reglas estáticas pasan por alto.

Los autores posicionan a NeuroAbs no como un reemplazo para los model checkers existentes, sino como un marco complementario que mejora su eficiencia. Los resultados demuestran que, incluso cuando se integra con model checkers altamente optimizados y ganadores de competencias (AVR y RIC3), el enfoque neuro-simbólico produce mejoras medibles tanto en la velocidad de construcción de la prueba como en la profundidad de detección de errores. El marco se presenta como un paso hacia una verificación de hardware más automatizada y consciente del escenario que reduce la dependencia de la intervención manual experta.