Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

Imagine que você está construindo um castelo enorme e intrincado feito de peças de Lego digitais. É isso que os engenheiros fazem quando projetam chips de computador: eles escrevem um código chamado RTL (Register Transfer Level) que diz como os minúsculos transistores devem se comportar. Mas aqui está o problema: se apenas uma peça for colocada no lugar errado, todo o castelo pode desmoronar quando a energia for ligada. Verificar esses erros é a parte mais difícil do trabalho, muitas vezes consumindo mais da metade do tempo. Tradicionalmente, os engenheiros usam duas formas principais para verificar seu trabalho. A primeira é como um "test drive", onde eles testam o chip através de alguns cenários específicos para ver se ele quebra. A segunda é a "verificação formal", que é como uma prova supermatemática que garante que o castelo resistirá sob todas as condições possíveis, não apenas as que eles testaram. No entanto, esse método de superprova geralmente exige softwares caros e restritos que apenas grandes empresas podem pagar.

Entra em cena o novo integrante do grupo: os Modelos de Linguagem de Grande Escala (LLMs). Você pode conhecê-los como os chatbots de IA que conseguem escrever histórias ou códigos. Recentemente, as pessoas começaram a perguntar: "Pode uma IA ser o arquiteto que conserta nossos castelos digitais quebrados?" A grande questão é se uma IA pode não apenas detectar um erro, mas também consertá-lo de uma forma que seja matematicamente provada como perfeita, sem a necessidade de comprar uma licença de software de um milhão de dólares. Este artigo mergulha nessa questão, tentando construir uma ponte entre a criatividade da IA e a lógica estrita e implacável da matemática formal, usando apenas ferramentas gratuitas e de código aberto.

O Detetive de IA e a Caixa de Ferramentas de Código Aberto

Neste estudo, um pesquisador chamado Ha Trung Tran construiu uma equipe inteligente de agentes de IA para atuar como uma equipe de reparo para designs de chips quebrados. Pense nisso como um esquadrão de detetives de alta tecnologia trabalhando em um ciclo. Em vez de uma única IA tentar fazer tudo de uma vez, a equipe é dividida: um agente lê as plantas, outro escreve as regras do que o chip deve fazer, um terceiro verifica o trabalho e um quarto realmente conserta o código.

O ingrediente secreto aqui é como eles verificam os erros. A maioria das ferramentas de reparo de IA apenas executa alguns test drives (simulações) para ver se o chip funciona. Mas esta equipe usa um "backend formal" — um motor matemático gratuito e de código aberto composto por ferramentas chamadas Yosys, SymbiYosys e Z3. Este motor não apenas adivinha; ele tenta provar matematicamente que o chip está correto. Se o chip falhar, o motor não diz apenas "está quebrado". Ele entrega à IA um "contraexemplo" específico, que é como uma reprodução de vídeo mostrando exatamente como o castelo desmoronou. A IA então assiste a esse vídeo, entende o que deu errado e tenta consertar o erro. Eles continuam fazendo isso — verificar, encontrar a falha, consertar, verificar novamente — até que a matemática prove que o chip é perfeito ou que fiquem sem tentativas.

A Boa Notícia: Funciona (Às Vezes)

Os pesquisadores testaram este sistema em seis tipos diferentes de designs digitais, variando de uma parte simples de calculadora (um ALU) a controladores de tráfego e unidades de memória mais complexos. Os resultados foram uma mistura de triunfo e limitações claras.

A estrela do show foi o ALU (Unidade Lógica e Aritmética), que é como o cérebro de calculadora de um chip. Os pesquisadores o quebraram propositalmente, trocando uma operação "AND" por uma operação "OR". A equipe de IA detectou o erro imediatamente. Em apenas duas rodadas de verificação e conserto, eles repararam o código. Mais importante ainda, o motor matemático de código aberto provou com 100% de certeza que o conserto estava correto para todos os números possíveis que o chip poderia processar. Isso aconteceu em todas as cinco rodadas de teste, levando uma média de apenas 16,5 segundos. Provou que a ideia funciona: uma IA, guiada por ferramentas matemáticas de código aberto, pode encontrar e consertar um bug real com uma garantia matemática.

A Má Notícia: Onde a IA Travou

No entanto, a história não é uma vitória total. Quando os pesquisadores tentaram o mesmo processo nos outros cinco designs, a equipe de IA encontrou um muro. Eles não conseguiram consertá-los de forma confiável. O artigo detalha cuidadosamente o porquê de terem falhado, identificando quatro "modos de falha" distintos que agem como armadilhas para a IA:

1. A Armadilha do "Muito Profundo" (Vacuidade de Cobertura Limitada): Em um caso (um contador), o motor matemático disse "FALHA" mesmo que o conserto fosse, na verdade, correto. Por quê? Porque o design precisava rodar por 256 ciclos para atingir um estado específico, mas a ferramenta só olhou 256 ciclos de profundidade. Era como tentar provar que um carro pode atravessar o país dirigindo apenas um quilômetro; a ferramenta não conseguiu ver o destino, então desistiu. O artigo observa que isso é um limite da ferramenta, não da IA.
2. A Armadilha das "Instruções Confusas" (Ambiguidade de Especificação): Para outro design (um árbitro), a IA tentou seguir as regras escritas, mas as regras pediam algo impossível (como um semáforo que muda sem um relógio). A IA seguiu fielmente as instruções impossíveis, levando a um beco sem saída.
3. A Armadilha da "Viagem no Tempo" (Bugs de Lógica Temporal): Em dois casos (um transmissor UART e uma memória FIFO), os bugs envolviam eventos acontecendo ao longo de múltiplos passos de tempo. A IA foi ótima em consertar a lógica de passo único (como a calculadora), mas teve dificuldade em raciocinar sobre sequências de eventos que aconteciam ao longo do tempo.
4. A Armadilha de "Muitas Regras" (Pressão de Propriedade Múltipla): No caso final (um escravo AXI Lite), havia tantas regras que o chip tinha que seguir simultaneamente que consertar uma regra quebrava outra. A IA ficou presa em um loop, incapaz de encontrar uma solução que satisfizesse a todos.

Um Bug Escondido na Caixa de Ferramentas

Houve também uma descoberta surpreendente sobre as próprias ferramentas de código aberto. Os pesquisadores descobriram que a ferramenta Yosys, que ajuda a processar o código, possui uma peculiaridade oculta. Se você tentar anexar as verificações de segurança (asserções) ao design usando um método específico chamado "bind", a ferramenta simplesmente ignora essas verificações. É como colocar uma câmera de segurança em uma sala, mas a câmera estar desconectada; o sistema pensa que está tudo bem porque nunca vê a câmera. Os pesquisadores tiveram que mudar seu método para "injetar" as verificações diretamente no código para garantir que o motor matemático realmente as visse. Esta é uma dica útil para qualquer pessoa que utilize essas ferramentas gratuitas.

Conclusão

Este artigo é um "estudo de viabilidade", que é uma forma elegante de dizer: "Nós tentamos, e aqui está exatamente onde funciona e onde falha". A principal conclusão é que é possível usar uma IA para consertar designs de chips com uma prova matemática de correção, mas apenas se você usar ferramentas de código aberto e se o problema não for complexo demais.

O autor é honesto sobre os limites: o sistema é ótimo para consertar erros de lógica simples e imediatos (como a calculadora), mas atualmente tem dificuldades com questões de tempo complexas, estados de memória profundos ou designs com regras conflitantes. Eles não alegaram ter resolvido o problema do reparo de chips; em vez disso, desenharam um mapa claro mostrando a "zona segura" onde a IA funciona e a "zona de perigo" onde ela se perde. Ao usar apenas ferramentas gratuitas, eles esperam reduzir o custo de entrada para esse tipo de pesquisa, provando que não é necessário um orçamento de um milhão de dólares para começar a construir o futuro do design de hardware confiável.