From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

Resumo Técnico: ProofLoop – Da Linguagem à Lógica

Título Original: From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

1. O Problema (Contexto e Motivação)

A verificação baseada em asserções (ABV) é fundamental para garantir a integridade de designs de hardware digital. O uso de SystemVerilog Assertions (SVA) permite que engenheiros expressem intenções de design que podem ser provadas formalmente. No entanto, a criação manual de SVAs é uma tarefa extremamente complexa, exigindo profundo conhecimento de lógica temporal e da semântica do nível de transferência de registradores (RTL).

Embora Modelos de Linguagem de Grande Escala (LLMs) tenham mostrado potencial para automatizar essa tarefa, as abordagens atuais falham por três motivos principais:

• Referências de sinais incorretas: Os modelos não conhecem a hierarquia real do hardware.
• Falta de metadados estruturais: LLMs não têm acesso nativo a informações como domínios de clock, tipos de reset (síncrono vs. assíncrono) ou relações de fan-in/fan-out.
• Inconsistências temporais: Dificuldade em alinhar a especificação em linguagem natural com o comportamento temporal exato do hardware.

2. Metodologia (O Framework ProofLoop)

Os autores propõem o ProofLoop, um agente baseado na arquitetura ReAct (Reasoning + Acting) que utiliza uma abordagem de "solver-in-the-loop" (solucionador no ciclo de feedback), integrando a ferramenta formal Cadence JasperGold. O processo é dividido em três etapas principais:

• A. Indexação AST e Base de Conhecimento: O design RTL é processado por um compilador para gerar uma Árvore de Sintaxe Abstrata (AST). Esta árvore é decomposta em quatro tipos semânticos (Interfaces de Módulo, Blocos Always, Instâncias e Atribuições Contínuas) e armazenada em um banco de dados vetorial para permitir a Recuperação Aumentada por Geração (RAG).
• B. Fase A - Coleta de Contexto (Agente ReAct): O agente opera em um loop de Pensamento $\rightarrow$ Ação $\rightarrow$ Observação. Ele decide autonomamente quais ferramentas invocar:
  • Ferramentas de Recuperação: Realizam buscas semânticas no banco de dados vetorial para encontrar lógica relevante.
  • Ferramentas de Análise Estrutural: Interagem com o JasperGold para extrair metadados que o texto do RTL não revela facilmente, como cones de dependência de sinais e propriedades de flip-flops.
• C. Fase B - Geração e Refinamento de SVA: O agente gera o SVA e o submete ao JasperGold. Se a ferramenta encontrar erros de sintaxe, sinais inexistentes ou se a asserção for falsificada, o erro e o contraexemplo são enviados de volta ao agente. O agente então realiza edições localizadas (em vez de regenerar tudo do zero) para corrigir o código até que ele seja provado ou atinja o limite de tentativas.

3. Principais Contribuições

1. Síntese de Contexto Agêntica: Um sistema que não segue um pipeline fixo, mas decide dinamicamente quais ferramentas de EDA (Electronic Design Automation) usar para entender o design.
2. Refinamento com Solver-in-the-loop: Integração iterativa com ferramentas formais para correção automática de erros baseada em feedback real de prova.
3. Escalabilidade para Designs Complexos: Uso de RAG e análise estrutural para lidar com designs multi-módulo que excedem a janela de contexto de LLMs tradicionais.

4. Resultados Experimentais

Os autores avaliaram o ProofLoop no benchmark FVEval (Design2SVA) utilizando o modelo Qwen3.5-35B.

• Desempenho Geral: O framework alcançou 93,7% de correção sintática e 82,0% de correção funcional, superando significativamente o método de prompting direto (que obteve apenas 43,2% de funcionalidade).
• Estudo de Ablação: Confirmou que cada componente é vital. A remoção do loop de verificação ou das ferramentas de análise estrutural causou quedas drásticas na precisão, provando que o feedback do solver e o conhecimento do hardware são os maiores diferenciais.
• Complexidade do Design: O ProofLoop mostrou-se mais robusto à medida que o design cresce. Enquanto modelos base degradam em designs com muitos módulos, o ProofLoop mantém a estabilidade devido à sua capacidade de busca granular via AST.
• Capacidade de Recuperação: O sistema foi altamente eficaz em corrigir erros de sintaxe (59,3% de recuperação), embora a correção de erros de lógica temporal (falsificações) ainda seja um desafio mais complexo para o modelo.

5. Significância

O trabalho representa um avanço importante na convergência entre IA e Verificação de Hardware. Ao transformar o LLM de um simples "gerador de texto" em um "agente de engenharia" que interage com ferramentas de EDA profissionais, o ProofLoop reduz a barreira de entrada para a verificação formal e oferece uma solução escalável para a crescente complexidade dos sistemas em chip (SoC).