Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

Resumen Técnico: Grafos de Conocimiento, el eslabón perdido en la verificación formal basada en IA Agéntica

Declaración del Problema
Si bien los Modelos de Lenguaje Grandes (LLM) han demostrado potencial en la generación de Aserciones SystemVerilog (SVAs) a partir de especificaciones en lenguaje natural para acelerar la Verificación Formal (FV), persisten obstáculos significativos. El desafío principal es el problema de "anclaje" (grounding): las especificaciones suelen ser ambiguas o incompletas, mientras que los detalles micro-arquitectónicos críticos residen en el código de Nivel de Transferencia de Registros (RTL). Los enfoques existentes tratan típicamente las especificaciones y el RTL como texto poco estructurado, lo que conduce a un anclaje débil entre especificación y RTL. Esto resulta en desajustes semánticos, fallos de sintaxis frecuentes durante el análisis formal y aserciones que requieren corrección iterativa extensa y triaje manual. Además, los métodos anteriores a menudo fallan en integrar persistentemente la retroalimentación de herramientas formales (como Contrajemplos o CEXs e informes de cobertura) en el bucle de generación, limitando el refinamiento sistemático.

Metodología
Los autores proponen una metodología centrada en la verificación que construye un Grafo de Conocimiento (KG) a partir de Representaciones Intermedias (IRs) estructuradas para cerrar la brecha entre la intención y la implementación. El flujo de trabajo se organiza en cuatro capas: Entradas, IRs JSON tipadas, KGs en tiempo de ejecución y Orquestación de Agentes.

1. Representaciones Intermedias (IRs): El sistema extrae y normaliza datos en artefactos JSON tipados, incluyendo spec_chunks.json (especificaciones jerárquicas), requirements.json, design_model.json (metadatos RTL como jerarquías y señales), properties.json y resultados de verificación (formal_results.json, cex_cases.json, coverage_metrics.json).
2. Construcción del Grafo de Conocimiento: Estas IRs se exportan como nodos y aristas para construir un KG en tiempo de ejecución utilizando NetworkX. El KG actúa como un registro de artefactos, vinculando requisitos, jerarquía de diseño, señales, suposiciones y propiedades. Permite la recuperación de contexto acotado; por ejemplo, al generar una propiedad, el KG proporciona el requisito específico, su fragmento de especificación padre, las señales RTL relevantes y los manuales de reglas.
3. Orquestación Multi-Agente: El proceso de verificación se descompone en agentes especializados que consultan y actualizan el KG:
   • Generación de Propiedades: Un agente líder coordina a un spec_analyst (descomponiendo requisitos), un sva_author (sintetizando sintaxis SVA), un sva_reviewer (validando adherencia) y un sva_patcher (corrigiendo basándose en retroalimentación).
   • Corrección de Sintaxis: Un bucle dedicado maneja errores de compilación. Los agentes analizan diagnósticos, aplican reparaciones deterministas para patrones comunes (por ejemplo, identificadores no declarados) y utilizan contexto complejo (declaraciones RTL, texto de requisitos) para errores más difíciles. Se permite un máximo de tres intentos de corrección para las propiedades.
   • Corrección de CEX: Cuando las propiedades fallan, los agentes analizan formas de onda VCD y trazas de fallo. Una clase spec_assertion_analyzer clasifica las causas raíz (por ejemplo, errores RTL vs. subespecificación), y un cex_fixer ajusta restricciones o fortalece aserciones.
   • Mejora de Cobertura: Los agentes analizan métricas de cobertura para identificar código inalcanzable o propiedades vacías, generando propiedades dirigidas para cerrar brechas.

Contribuciones Clave
El artículo afirma tres contribuciones principales:

1. Construcción de KG Centrada en Verificación: Un enfoque novedoso que construye un KG a partir de IRs estructuradas que integra la intención de especificación, la estructura RTL, las propiedades generadas y los resultados de herramientas formales en un único artefacto consultable.
2. Flujo de Trabajo Multi-Agente con Trazabilidad: Un sistema donde los agentes utilizan contexto anclado al KG para generar y refinar SVAs, manteniendo enlaces de trazabilidad explícitos desde requisitos hasta elementos de diseño, propiedades y resultados de verificación.
3. Evaluación Empírica: Una evaluación en siete diseños de referencia de código abierto que cuantifica el impacto del contexto anclado al KG en la efectividad de la generación de propiedades, la validez sintáctica y la eficacia de los bucles de refinamiento de CEX.

Resultados
La metodología se evaluó en siete diseños (FIFO, Lemming, ALU, CICD, BST, Contador TTC y CSR) utilizando el modelo GPT-5.2 y Cadence JasperGold.

• Sintaxis y Compilación: El enfoque produjo consistentemente SVAs compilables con una sobrecarga baja de reparación de sintaxis. El contexto anclado al KG, particularmente la resolución determinista de señales y jerarquía a través de la IR design_model, redujo significativamente problemas de front-end como identificadores no declarados.
• Cobertura Formal: La cobertura formal de extremo a extremo osciló entre el 78.5% y el 99.4% en los puntos de referencia.
• Eficacia de Refinamiento: Diseños como FIFO y CIC Decimator mostraron una mejora significativa después de los bucles de CEX y cobertura, lo que sugiere que muchos fallos iniciales se debieron a problemas locales (guardas faltantes, condiciones de límite) corregibles mediante contexto recuperado.
• Limitaciones: La convergencia dependió del diseño. Diseños complejos como el Árbol de Búsqueda Binaria (BST) y aquellos que requieren invariantes globales o razonamiento temporal profundo (por ejemplo, Lemming, ALU) mostraron una mejora limitada con la corrección automatizada. Los autores señalan que las capacidades actuales de los LLM luchan con el razonamiento temporal y aritmético complejo, y la depuración semántica sigue siendo el principal cuello de botella para los puntos de referencia más difíciles.

Significancia
El artículo postula que el enfoque centrado en KG propuesto aborda la debilidad crítica de trabajos anteriores: la falta de enlaces estructurados y consultables entre requisitos, semántica RTL y resultados de verificación. Al tratar la retroalimentación de herramientas formales (CEXs, brechas de cobertura) como contenido persistente y consultable del KG en lugar de salidas transitorias, el sistema permite un proceso de refinamiento de bucle cerrado. Los autores concluyen que, si bien la corrección semántica para razonamiento complejo sigue siendo un desafío, este marco proporciona una base robusta para la generación de propiedades trazable y fundamentada en el diseño. A medida que avancen las capacidades de los LLM, estarán mejor posicionados para aprovechar el contexto estructurado y las trazas proporcionadas por este KG, mejorando aún más la fiabilidad de la verificación formal automatizada.