Autoformalizing Memory Specifications with Agents

1. Formulação do Problema

A fase de Verificação de Design (DV) do projeto de chips semicondutores é um grande gargalo, consumindo mais de 50% do ciclo de vida do projeto. O desafio central reside na tradução de especificações de linguagem natural não estruturadas (por exemplo, padrões JEDEC para chips de memória) em modelos formais e executáveis necessários para a verificação.

As abordagens atuais de IA geralmente focam na geração de Assertivas SystemVerilog (SVAs) isoladas. No entanto, essa abordagem apresenta limitações significativas:

• Incompletude: As SVAs verificam propriedades específicas, mas não geram modelos comportamentais completos, geradores de estímulo ou métricas de cobertura funcional.
• Ambiguidade: Especificações em linguagem natural frequentemente contêm ambiguidades que levam os LLMs a gerar assertivas sintaticamente inválidas ou desalinhadas com o protocolo.
• Complexidade: Padrões modernos de memória (DDR5, HBM3, GDDR7) envolvem restrições de temporização intrincadas, interações complexas de comandos e estruturas hierárquicas que são difíceis de capturar com uma geração simples de prompt para código.

2. Metodologia

Os autores propõem um Framework de Autoformalização Agente que converte especificações de memória em linguagem natural em uma representação intermediária estruturada e executável chamada DRAMPyML, em vez de gerar SVAs diretamente.

2.1 A Representação Intermediária: DRAMPyML

Em vez de saltar diretamente para assertivas, o sistema visa o DRAMPyML, uma linguagem de modelagem baseada em Python construída sobre Redes de Petri Temporizadas.

• Estrutura: Modela dispositivos de memória como uma tupla de lugares (bancos, ranks), transições (comandos como ACT, RD, WR) e arcos (regulares, inibidores, reset e temporizados).
• Vantagens: Esta representação é executável, permitindo a geração de traços de comando, estímulos e verificações de temporização. Serve como uma fonte unificada da qual SVAs, bancadas de teste e modelos de cobertura podem ser derivados a jusante.
• Definições Formais: O artigo define redes de Petri DRAM matematicamente e introduz o conceito de Equivalência de Traço. Ele postula (e valida empiricamente) a Conjectura 3.4: que verificar a equivalência de traços para pequenas configurações (por exemplo, 1 ou 2 bancos) com comprimentos de traço curtos ($k=4$) é suficiente para provar a equivalência para o dispositivo completo e complexo devido às propriedades de simetria.

2.2 O Agente de Autoformalização

O sistema emprega um Fluxo de Trabalho Agente iterativo (Figura 2 no artigo) em vez de uma abordagem de geração única:

1. Entrada: O agente recebe especificações em PDF da JEDEC, folhas de dados de fabricantes e a biblioteca DRAMPyML.
2. Loop Iterativo: O agente utiliza ferramentas (servidores MCP, APIs de LLM) para:
   • Ler seções específicas da especificação.
   • Escrever ou editar código Python para construir o grafo da Rede de Petri.
   • Auto-Validar: Executar testes de validação internos (verificando deadlocks, nós órfãos e gerando traços de comando para cruzar com a especificação).
3. Refinamento: Com base no feedback de validação, o agente refina iterativamente o modelo até que a consistência estrutural e a correção de temporização sejam satisfeitas.
4. Estratégias de Prompting: O estudo compara o prompting One-Shot (único prompt com convenções explícitas) versus Agente (interação iterativa com o ambiente e ferramentas).

3. Contribuições Principais

1. DRAMBench: O lançamento do primeiro benchmark de código aberto para autoformalização de hardware, contendo formalizações DRAMPyML de verdade para 13 padrões JEDEC (cobrindo DDR2-5, LPDDR2-5, GDDR5-7 e HBM2-3).
2. Framework Agente: Demonstração de que um agente iterativo usando validação aumentada por ferramentas supera significativamente a geração one-shot, particularmente para especificações complexas.
3. Validação Teórica e Empírica:
   • Definição formal de redes de Petri DRAM e equivalência de traço.
   • Prova empírica de que verificar traços curtos ($k \le 4$) em configurações mínimas (1-2 bancos) é suficiente para detectar bugs semânticos nos modelos gerados, contornando o problema da explosão do espaço de estados.
4. Resultados de Benchmarking: Uma avaliação abrangente de modelos state-of-the-art (Sonnet 4.5, GPT-5.2, DeepSeek-v3p2) mostrando os trade-offs entre custo de tokens e desempenho.

4. Resultados Experimentais

Os autores avaliaram os modelos no conjunto de dados DRAMBench usando duas métricas:

• Índice Jaccard: Mede a sobreposição de traços de comando legais entre o modelo gerado e a verdade fundamental (ground truth).
• Recall de Restrição de Temporização: Mede a fração de restrições de temporização da verdade fundamental corretamente recuperadas.

Principais Descobertas:

• Agente vs. One-Shot: A abordagem agente alcançou consistentemente um desempenho de pico mais alto, especialmente para padrões complexos (por exemplo, DDR5, HBM3) e quando nenhum exemplo foi fornecido. A geração one-shot lutou com o formato de saída não familiar sem priores fortes.
• Impacto dos Exemplos: Fornecer exemplos "selecionados" (por exemplo, usar DDR3 para ajudar a gerar DDR4) aumentou significativamente o desempenho para ambos os métodos, às vezes permitindo que modelos one-shot superassem agentes em tarefas mais simples.
• Desempenho do Modelo:
  • DeepSeek-v3p2 (pesos abertos) performou competitivamente com modelos de código fechado (Sonnet 4.5, GPT-5.2), muitas vezes superando-os no cenário agente.
  • Sonnet 4.5 alcançou a perfeição estrutural mais alta para padrões como HBM2 e DDR2-4 quando fornecido com exemplos.
• Modos de Falha: A análise de falhas complexas (por exemplo, DDR5) revelou que agentes lutam com:
  • Selecionar primitivas corretas (por exemplo, comandos de pré-carga errados).
  • Modelar hierarquia de memória (por exemplo, grupos de bancos).
  • Impor restrições de temporização no nível de abstração correto (mismatches de coordenadas causando arcos de temporização a se tornarem inativos).
• Eficiência de Tokens: Embora agentes alcancem maior precisão, eles consomem mais tokens. No entanto, para especificações complexas, a curva "token vs. desempenho" favorece o agente, pois modelos one-shot falham em convergir para estruturas corretas independentemente da contagem de tokens.

5. Significado

Este trabalho representa uma mudança de paradigma na verificação de hardware:

• De Assertivas para Modelos: Avança além da geração de assertivas isoladas para a criação de modelos comportamentais estruturados e executáveis. Isso permite um "shift-left" na verificação, permitindo a detecção precoce de falhas de design e a geração automática de colateral diverso (estímulo, cobertura, SVAs).
• Escalabilidade: Ao aproveitar a representação intermediária DRAMPyML e a verificação de equivalência de traço, o método oferece um caminho escalável para verificar dispositivos de memória modernos e altamente paralelos que anteriormente eram complexos demais para autoformalização automatizada.
• Ciência Aberta: O lançamento do DRAMBench fornece um benchmark padronizado e de nível profissional que anteriormente faltava na literatura de IA para Hardware, permitindo que a comunidade acompanhe o progresso na autoformalização de hardware.

Em conclusão, o artigo demonstra que fluxos de trabalho agentes combinados com representações intermediárias estruturadas (Redes de Petri) são o caminho mais viável para automatizar a verificação de padrões complexos de semicondutores, superando as limitações das abordagens atuais de LLM direto para assertiva.