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

Resumo Técnico: Grafos de Conhecimento, o Elo Perdido na Verificação Formal Baseada em IA Agêntica

Declaração do Problema
Embora os Modelos de Linguagem de Grande Porte (LLMs) tenham demonstrado potencial na geração de Asserções em SystemVerilog (SVAs) a partir de especificações em linguagem natural para acelerar a Verificação Formal (FV), obstáculos significativos permanecem. O desafio principal é o problema da "fundamentação" (grounding): as especificações são frequentemente ambíguas ou incompletas, enquanto detalhes micro-arquiteturais críticos residem no código de Nível de Transferência de Registradores (RTL). Abordagens existentes tipicamente tratam especificações e RTL como texto pouco estruturado, levando a uma fundamentação fraca entre especificação e RTL. Isso resulta em incompatibilidades semânticas, falhas frequentes de sintaxe durante a análise formal e asserções que exigem correção iterativa extensa e triagem manual. Além disso, métodos anteriores frequentemente falham em integrar persistentemente o feedback de ferramentas formais (como Contraexemplos ou CEXs e relatórios de cobertura) no ciclo de geração, limitando o refinamento sistemático.

Metodologia
Os autores propõem uma metodologia centrada na verificação que constrói um Grafo de Conhecimento (KG) a partir de Representações Intermediárias (IRs) estruturadas para fechar a lacuna entre intenção e implementação. O fluxo de trabalho é organizado em quatro camadas: Entradas, IRs em JSON Tipado, KGs em Tempo de Execução e Orquestração de Agentes.

1. Representações Intermediárias (IRs): O sistema extrai e normaliza dados em artefatos JSON tipados, incluindo spec_chunks.json (especificações hierárquicas), requirements.json, design_model.json (metadados de RTL como hierarquias e sinais), properties.json e resultados de verificação (formal_results.json, cex_cases.json, coverage_metrics.json).
2. Construção do Grafo de Conhecimento: Essas IRs são exportadas como nós e arestas para construir um KG em tempo de execução usando NetworkX. O KG atua como um registro de artefatos, vinculando requisitos, hierarquia de design, sinais, premissas e propriedades. Ele permite recuperação de contexto delimitado; por exemplo, ao gerar uma propriedade, o KG fornece o requisito específico, seu fragmento de especificação pai, sinais de RTL relevantes e manuais de regras.
3. Orquestração Multi-Agente: O processo de verificação é decomposto em agentes especializados que consultam e atualizam o KG:
   • Geração de Propriedades: Um agente líder coordena um spec_analyst (decompondo requisitos), um sva_author (sintetizando sintaxe SVA), um sva_reviewer (validando aderência) e um sva_patcher (corrigindo com base no feedback).
   • Correção de Sintaxe: Um loop dedicado trata erros de compilação. Agentes analisam diagnósticos, aplicam reparos determinísticos para padrões comuns (por exemplo, identificadores não declarados) e usam contexto complexo (declarações de RTL, texto de requisito) para erros mais difíceis. As propriedades têm um máximo de três tentativas de correção.
   • Correção de CEX: Quando as propriedades falham, os agentes analisam formas de onda VCD e trilhas de falha. Um spec_assertion_analyzer classifica as causas raiz (por exemplo, bugs de RTL versus subespecificação), e um cex_fixer ajusta restrições ou fortalece asserções.
   • Melhoria de Cobertura: Agentes analisam métricas de cobertura para identificar código inacessível ou propriedades vazias, gerando propriedades direcionadas para fechar lacunas.

Principais Contribuições
O artigo reivindica três contribuições primárias:

1. Construção de KG Centrada em Verificação: Uma abordagem inovadora que constrói um KG a partir de IRs estruturadas, integrando intenção de especificação, estrutura de RTL, propriedades geradas e resultados de ferramentas formais em um único artefato consultável.
2. Fluxo de Trabalho Multi-Agente com Rastreabilidade: Um sistema onde agentes usam contexto fundamentado no KG para gerar e refinar SVAs, mantendo links de rastreio explícitos desde requisitos até elementos de design, propriedades e resultados de verificação.
3. Avaliação Empírica: Uma avaliação em sete designs de referência de código aberto quantificando o impacto do contexto fundamentado no KG na eficácia da geração de propriedades, validade sintática e eficácia dos ciclos de refinamento de CEX.

Resultados
A metodologia foi avaliada em sete designs (FIFO, Lemming, ALU, CICD, BST, Contador TTC e CSR) usando o modelo GPT-5.2 e o Cadence JasperGold.

• Sintaxe e Compilação: A abordagem produziu consistentemente SVAs compiláveis com baixa sobrecarga de reparo de sintaxe. O contexto fundamentado no KG, particularmente a resolução determinística de sinais e hierarquia via IR design_model, reduziu significativamente problemas de front-end como identificadores não declarados.
• Cobertura Formal: A cobertura formal de ponta a ponta variou de 78,5% a 99,4% entre as referências.
• Eficácia de Refinamento: Designs como FIFO e CIC Decimator mostraram melhoria significativa após ciclos de CEX e cobertura, sugerindo que muitas falhas iniciais foram devidas a problemas locais (guardas ausentes, condições de limite) corrigíveis via contexto recuperado.
• Limitações: A convergência dependeu do design. Designs complexos como a Árvore de Busca Binária (BST) e aqueles que exigem invariantes globais ou raciocínio temporal profundo (por exemplo, Lemming, ALU) mostraram melhoria limitada com correção automatizada. Os autores observam que as capacidades atuais dos LLMs lutam com raciocínio temporal e aritmético complexo, e a depuração semântica permanece o principal gargalo para referências mais difíceis.

Significância
O artigo postula que a abordagem centrada no KG proposta aborda a fraqueza crítica de trabalhos anteriores: a falta de links estruturados e consultáveis entre requisitos, semântica de RTL e resultados de verificação. Ao tratar o feedback de ferramentas formais (CEXs, lacunas de cobertura) como conteúdo persistente e consultável do KG, em vez de saídas transitórias, o sistema permite um processo de refinamento em ciclo fechado. Os autores concluem que, embora a correção semântica para raciocínio complexo permaneça um desafio, este framework fornece uma base robusta para geração de propriedades rastreável e fundamentada no design. À medida que as capacidades dos LLMs avançam, eles estarão melhor posicionados para aproveitar o contexto estruturado e os rastros fornecidos por este KG, melhorando ainda mais a confiabilidade da verificação formal automatizada.