Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

En el mundo invisible de los microchips, donde miles de millones de transistores se encienden y apagan para alimentar desde teléfonos inteligentes hasta naves espaciales, un solo error oculto puede causar que un sistema falle catastróficamente. Los ingenieros diseñan estos chips utilizando un lenguaje llamado Nivel de Transferencia de Registros, o RTL, que describe cómo se mueven los datos entre elementos de almacenamiento a lo largo del tiempo. Para asegurar que estos diseños funcionen correctamente antes de ser construidos, los expertos en verificación escriben "aserciones". Piense en una aserción como una regla estricta escrita en el propio diseño, una declaración que dice: "Si esto sucede, entonces aquello debe seguir". Si el chip llegara a violar esta regla, el sistema activa una alarma, revelando un error que de otro modo podría pasar desapercibido. Durante décadas, escribir estas reglas ha sido una tarea lenta, manual y propensa a errores, que requiere que los ingenieros adivinen qué comportamientos podrían fallar y escriban comprobaciones específicas para ellos. Aunque las computadoras han ayudado mediante la minería de simulaciones de diseño existentes para encontrar patrones, estos métodos automatizados suelen perder los escenarios más peligrosos simplemente porque las pruebas aleatorias en las que confían nunca llegan a tropezar con ellos.

Un equipo de investigadores de la Universidad de Ciencia y Tecnología de Hong Kong (Guangzhou) ha desarrollado un nuevo enfoque para resolver este problema, llamando a su sistema NeuroAssertion. En lugar de depender del azar para encontrar errores, su método busca activamente los comportamientos más difíciles de alcanzar en un diseño de chip y luego utiliza una combinación de inteligencia artificial y lógica formal para escribir las reglas de seguridad necesarias. El proceso comienza transformando el diseño para que sea más fácil ver qué partes están siendo probadas. Los investigadores insertan marcadores especiales en el código que rastrean si ciertas condiciones difíciles de activar alguna vez han ocurrido. Luego, utilizan un potente motor matemático, conocido como verificador de modelos (model checker), para forzar al diseño a ejecutar esas condiciones raras. Esto genera un conjunto de casos de prueba altamente específicos que exponen comportamientos que las simulaciones aleatorias probablemente perderían para siempre. Estos nuevos y diversos rastros proporcionan una base mucho más rica para el siguiente paso.

Una vez que el sistema tiene estos comportamientos difíciles de encontrar, pasa a la fase de generación. Utiliza una técnica llamada síntesis guiada por sintaxis para crear reglas de seguridad iniciales basadas en los datos observados. Sin embargo, los investigadores reconocieron que este primer paso rara vez es perfecto. Para solucionar esto, introdujeron un bucle de refinamiento que actúa como un editor riguroso. El sistema mide qué tan bien el conjunto actual de reglas puede detectar cambios en el diseño inyectando errores pequeños y deliberados, conocidos como mutantes, en el código. Si las reglas no logran detectar un mutante, el sistema sabe exactamente qué comportamiento queda sin verificar. Entonces, recurre a un modelo de lenguaje de gran tamaño para proponer una nueva regla diseñada específicamente para cubrir ese vacío. Si la regla propuesta es lógicamente defectuosa, un segundo modelo de lenguaje no la descarta; en su lugar, analiza el error y construye un conjunto especializado de instrucciones, o gramática, para guiar a un resolvedor simbólico en la reparación de la regla. Esto crea un ciclo donde el sistema propone, comprueba y corrige aserciones hasta que son tanto numerosas como robustas.

Los resultados de este enfoque fueron probados en siete diseños de chips diferentes, que van desde pequeños circuitos de arbitraje hasta complejos núcleos de procesadores. El nuevo marco superó consistentemente al método anterior de vanguardia, conocido como SMART, que depende de una única pasada de minería sin este refinamiento activo. En estos experimentos, NeuroAssertion generó aproximadamente el doble de aserciones que el método anterior. Más importante aún, la calidad de estas reglas fue significativamente mayor. Al medirse por su capacidad para detectar errores inyectados, el nuevo sistema logró aproximadamente el doble de cobertura que el enfoque tradicional. En algunos bancos de pruebas específicos, la mejora fue incluso más dramática; por ejemplo, en un componente de procesador, la cobertura de mutación saltó de aproximadamente el seis por ciento a más del treinta y dos por ciento. Los investigadores también compararon su sistema contra un enfoque directo donde se le pidió a un modelo de lenguaje de gran tamaño que escribiera reglas sin ningún paso de comprobación formal o refinamiento. Ese método directo produjo muchas menos reglas y no logró detectar la mayoría de los errores potenciales, demostiendo que la generación de lenguaje pura por sí sola es insuficiente para esta tarea de alto riesgo.

Al tratar la generación de aserciones como un bucle continuo de exploración y refinamiento en lugar de un evento de una sola vez, los investigadores han demostrado que es posible automatizar la creación de reglas de seguridad de alta calidad para hardware complejo. El sistema no solo adivina; busca activamente los puntos ciegos en un diseño y utiliza una asociación entre redes neuronales y lógica formal para llenarlos. Este trabajo sugiere que el futuro de la verificación de hardware reside en combinar el reconocimiento de patrones de la inteligencia artificial con la certeza rigurosa de la prueba matemática, asegurando que los chips que impulsan nuestro mundo sean tan confiables como los ingenieros que los diseñan.