🤖 AI

Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation

Veri-Sure é um framework multiagente consciente de contratos que garante a correção de RTL em nível de silício ao alinhar a intenção dos agentes por meio de contratos de design, realizar reparos localizados precisos via fatiamento de dependência estática e validar saídas através de um pipeline híbrido de análise temporal baseada em traços e verificação formal, tudo avaliado no recém-introduzido benchmark de nível industrial VerilogEval-v2-EXT.

Autores originais: Jiale Liu, Taiyu Zhou, Tianqi Jiang

Publicado 2026-01-28

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Jiale Liu, Taiyu Zhou, Tianqi Jiang

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando construir uma máquina complexa e de alta velocidade (como um robô futurista) baseada em um conjunto de instruções escritas em inglês simples. Você pede a uma IA superinteligente para traduzir essas instruções nos projetos reais (código) para a máquina.

O problema é que a IA é ótima em escrever frases, mas frequentemente comete erros minúsculos e invisíveis nos projetos que só aparecem quando a máquina começa a funcionar em velocidade máxima. No mundo real do design de chips, esses erros são caros — podem custar milhões de dólares para corrigir depois que o chip é fabricado.

Este artigo apresenta o VERI-SURE, uma nova "equipe de especialistas em IA" projetada para corrigir esses erros antes mesmo de o chip ser construído. Veja como funciona, usando analogias simples:

1. O Problema: O "Telefone Sem Fio" e o "Ponto Cego"

Quando você pede a uma única IA para escrever código, duas coisas dão errado:

O Telefone Sem Fio: Se você pedir à IA para corrigir um erro (bug), ela pode entender mal o seu objetivo original. Ela altera o código para corrigir uma coisa, mas acidentalmente quebra a intenção original.
O Ponto Cego: A IA geralmente verifica seu trabalho executando uma simulação (um teste de direção). Mas, assim como um teste de direção pode não detectar uma falha rara no motor que só acontece em uma estrada específica e esburacada, a simulação frequentemente ignora erros de tempo complicados que só acontecem no mundo real.

2. A Solução: Uma Equipe de Construção Especializada

Em vez de uma única IA fazer tudo, o VERI-SURE estabelece uma equipe de construção onde cada membro tem um trabalho específico. Todos concordam com um "Contrato de Design" primeiro.

O Arquiteto (O Criador do Contrato): Antes de qualquer um escrever uma única linha de código, este agente traduz suas instruções desorganizadas em inglês para um "contrato" matemático rigoroso. Ele define exatamente como a máquina deve se comportar, o que os botões fazem e quão rápido ela deve rodar. Isso garante que todos na equipe estejam lendo o mesmo mapa.
O Programador (O Construtor): Este agente escreve os projetos reais (o código) baseando-se estritamente no contrato.
O Verificador (O Inspetor de Segurança): Este agente realiza o teste de direção (simulação). Se a máquina falhar, ele não diz apenas "Quebrou". Ele analisa os dados da colisão.

3. O Truque de Mágica: "Reparo Cirúrgico" vs. "Demolição"

Quando o teste de direção falha, sistemas de IA antigos costumam entrar em pânico e tentar demolir todo o edifício e começar do zero. Isso é arriscado porque eles podem esquecer como construir as paredes corretamente.

O VERI-SURE usa o Reparo Cirúrgico:

O Detetive (Análise de Traço): Ele observa os dados da "caixa preta" (formas de onda) para encontrar o segundo exato em que a máquina falhou.
O Cirurgião (Fatiamento de Dependência): Em vez de adivinhar, ele rastreia os fios para encontrar o exato pequeno bloco de código que está causando o problema. Ele isola essa pequena peça.
O Remendo: A IA reescreve apenas esse pequeno bloco quebrado. O resto da máquina permanece exatamente o mesmo. Isso evita o "Telefone Sem Fio", onde consertar uma coisa quebra outra.

4. A Superverificação: "Prova Matemática" vs. "Teste de Direção"

Às vezes, um teste de direção não é suficiente para provar que uma máquina é segura.

O Verificador de Regras (O Aplicador de Regras): Este agente verifica se a máquina segue as regras de tempo (ex: "A luz acendeu exatamente quando o botão foi pressionado?").
O Provador Booleano (O Mestre da Matemática): Para as partes lógicas, este agente não apenas executa testes; ele utiliza provas matemáticas para garantir que o código não pode estar errado, não importa quais entradas você forneça. É como provar que uma ponte nunca desabará usando equações de física, em vez de apenas dirigir um carro sobre ela uma vez.

5. A Nova Pista de Teste: "O Circuito de Obstáculos Difícil"

Para provar que sua equipe é a melhor, os autores construíram um novo circuito de obstáculos mais difícil chamado VERILOGEVAL-V2-EXT.

Os testes antigos eram como dirigir em um estacionamento (tarefas fáceis e curtas).
O novo teste inclui dirigir através de uma tempestade, navegar em um labirinto e lidar com carga pesada (tarefas de nível industrial, como protocolos de comunicação complexos e controle de memória).

O Resultado

Quando colocaram sua equipe (VERI-SURE) neste novo e difícil circuito de obstáculos:

IAs isoladas (os gênios solitários) acertaram cerca de 76% das tarefas.
Antigas equipes de IA (sem o reparo cirúrgico ou provas matemáticas) tiveram dificuldades com as tarefas mais difíceis.
O VERI-SURE alcançou 93% de sucesso, mesmo nas tarefas mais difíceis e complexas.

Em resumo: O VERI-SURE não apenas pede para uma IA "escrever código". Ele cria uma equipe disciplinada que concorda com um plano, conserta apenas as partes quebradas com cirurgia e usa a matemática para provar que o conserto é perfeito, garantindo que o chip final funcione exatamente como pretendido.

Resumo Técnico: VERI-SURE

1. Declaração do Problema

A implantação de Grandes Modelos de Linguagem (LLMs) para o design de Transferência de Registrador (RTL) em Automação de Projeto Eletrônico (EDA) enfrenta obstáculos significativos para alcançar a correção de nível de silício. Embora os LLMs tenham avançado na geração de código de software, a geração de RTL apresenta desafios únicos devido à natureza concorrente do hardware, ao rigor do tempo ao nível de ciclo e à semântica de protocolo. O artigo identifica três gargalos primários nos atuais pipelines de RTL baseados em LLM:

Confiabilidade de Avaliação Limitada: Avaliações centradas em simulação frequentemente sofrem de cobertura de teste insuficiente, falhando em capturar casos de borda temporais sutis.
Ineficiências de Depuração: A depuração iterativa leva frequentemente a "regressões e alucinações de reparo" causadas pela regeneração de arquivos inteiros, o que desestabiliza a lógica não relacionada.
Deriva Semântica: À medida que a intenção da linguagem natural é reinterpretada através de múltiplas transferências de agentes ou iterações, a intenção de design original pode degradar, levando a implementações inconsistentes.

Benchmarks existentes, como o VerilogEval-v2, são criticados por serem dominados por módulos pedagógicos curtos que sub-representam necessidades industriais, como unidades aritméticas avançadas, protocolos de comunicação e padrões de Cruzamento de Domínio de Clock (CDC).

2. Metodologia: O Framework VERI-SURE

O VERI-SURE é um framework multi-agente consciente de contrato projetado para fechar o ciclo entre síntese de código, verificação e reparo localizado. Ele vai além da tradução de etapa única para um ciclo automatizado de gerar-verificar-depurar.

Componentes Principais

Contrato de Design (Agente Arquiteto): O framework começa destilando especificações de linguagem natural em um contrato de design estruturado em formato JSON. Este contrato define explicitamente a semântica da interface, convenções de clock/reset, comportamento ciclo-preciso e casos de borda. Ele serve como uma "fonte da verdade" compartilhada para todos os agentes subsequentes para evitar a deriva semântica.
Fluxo de Trabalho Multi-Agente:
- Agente Programador (Coder Agent): Gera código RTL sintetizável baseado no contrato.
- Agente Verificador (Verifier Agent): Produz testbenches de auto-verificação alinhados com o contrato.
- Agente Depurador (Debugger Agent): Lidera o loop de depuração autônomo quando a simulação falha.
- Agente Asserter (Asserter Agent): Gera asserções SystemVerilog direcionadas para detectar violações sequenciais ou de protocolo (ex: amostragem de borda errada, incompatibilidade de reset).
- Agente de Prova Booleana (Boolean Proofer Agent): Realiza verificação formal em lógica combinacional para validar correções candidatas e prevenir regressões.

Mecanismos Chave

Análise Temporal Baseada em Traço & Fatiamento Estático: Quando a simulação falha, o sistema não depende apenas de logs textuais. Ele analisa formas de onda de Dump de Mudança de Valor (VCD) para identificar o tempo de divergência mais precoce ( $t_f$ ). Em seguida, emprega o fatiamento de dependência estática para computar o "cone de lógica" que influencia os sinais que falharam. Isso isola a falha a um conjunto mínimo de blocos de código suspeitos (intervalos de linhas), em vez de todo o arquivo.
Remendo Localizado (Localized Patching): Guiado pela análise de fatiamento, o agente Depurador aplica edições precisas de nível de bloco (ler/substituir) apenas aos blocos suspeitos. Isso evita a instabilidade de reescritas de arquivos inteiros. Uma regra de rollback garante que os patches sejam mantidos apenas se melhorarem a assinatura de falha (ex: tempo de primeira falha posterior ou menos incompatibilidades).
Verificação de Múltiplos Ramos: O framework integra dois ramos de verificação:
1. Análise Temporal Baseada em Traço: Para questões sequenciais e de tempo.
2. Verificação Formal: Combina verificação baseada em asserções (via Asserter) e provas de equivalência booleana (via Boolean Proofer usando SymbiYosus) para verificar restrições combinacionais e provar a correção além da simulação finita.

3. Benchmark: VERILOGEVAL-V2-EXT

Para avaliar melhor a geração de RTL de nível industrial, os autores introduzem o VERILOGEVAL-V2-EXT. Este benchmark estende o VerilogEval-v2 original adicionando 53 novas tarefas de design de nível industrial, trazendo o total para 209 problemas.

Conteúdo: As novas tarefas cobrem domínios complexos como protocolos de comunicação (UART, FIFO), aritmética avançada, núcleos de DSP e datapath de múltiplos ciclos.
Estratificação: Os problemas são classificados em níveis de dificuldade Fácil, Médio e Difícil baseados em sinais estruturais (linhas de código, número de blocos assign/always, largura de datapath) e revisão manual. Isso permite uma análise mais fina dos modos de falha.

4. Resultados Experimentais

Os autores avaliaram o VERI-SURE contra 15 LLMs independentes (incluindo modelos comerciais de código fechado e modelos de pesos abertos), loops de feedback de agente único e sistemas multi-agentes anteriores (MAGE, VerilogCoder).

Desempenho: O VERI-SURE alcançou um Pass@1 funcional de 93,30% no benchmark VERILOGEVAL-V2-EXT, com 100% de sucesso de sintaxe.
Tarefas Difíceis: O framework mostrou sua maior vantagem em tarefas "Difíceis", alcançando uma taxa de passagem funcional de 85,07%, superando significativamente o melhor modelo independente (Gemini-3-Pro com 62,69%) e outros baselines agênticos.
Agnosticismo de Backbone: Embora o VERI-SURE tenha performado melhor com o GPT-5.2, ele também impulsionou significativamente o desempenho do modelo de pesos abertos DeepSeek-3.2, elevando sua taxa de passagem funcional de 61,24% (standalone) para 71,29%.
Estudos de Ablação:
- Remover o mecanismo de Rastreamento, Fatiamento e Remendo (Tracing, Slicing, and Patching) causou a maior queda de desempenho (11,0% no total, 16,4% em tarefas Difíceis), confirmando que a localização precisa é crítica.
- Remover a Verificação Formal reduziu a taxa de passagem de tarefas Difíceis em 11,9 pontos percentuais, demonstrando sua necessidade para depurar bugs lógicos profundos que a simulação perde.
- O mecanismo de Contrato (Contract) contribuiu com uma queda de 2,9% no desempenho geral quando removido, destacando seu papel na manutenção da consistência de intenção.

5. Significância e Alegações

O artigo afirma que o VERI-SURE demonstra que o design de RTL automatizado pode se aproximar da "correção de nível de silício" ao mudar de uma avaliação centrada em simulação para uma abordagem híbrida combinando análise baseada em traço e verificação formal.

As principais alegações incluem:

Mitigação da Deriva Semântica: Ao impor um contrato de design estruturado, o framework alinha as intenções dos agentes e evita a reinterpretação gradual dos requisitos.
Estabilidade no Reparo: O mecanismo de remendo guiado pelo fatiamento de dependência reduz efetivamente os riscos de regressão e as alucinações de reparo associadas à regeneração de arquivos inteiros.
Além da Simulação: A integração de provas formais permite que o sistema verifique a correção funcional de maneiras que a simulação pura não consegue, particularmente para equivalência combinacional e restrições de tempo complexas.
Relevância Industrial: A introdução do VERILOGEVAL-V2-EXT fornece um ambiente de teste mais realista e discriminativo para avaliar capacidades de geração de RTL de ponta a ponta, abordando a lacuna entre benchmarks acadêmicos e requisitos de blocos de IP industrial.

Os autores concluem que, embora o pré-treinamento em larga escala forneça uma base forte, o fluxo de trabalho agêntico estruturado com verificação formal é essencial para alcançar alta confiabilidade em designs de hardware complexos de múltiplos ciclos.