🤖 AI

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus

O artigo apresenta o NoTB, um framework livre de oráculo que aproveita a verificação de equivalência sequencial através de múltiplos designs RTL gerados por LLM para estabelecer um sinal de consenso formal, permitindo uma triagem de alta precisão de correção funcional sem depender de testbenches ou referências de ouro.

Autores originais: Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

Publicado 2026-08-25

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

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

No mundo do design de chips de computador, os engenheiros tradicionalmente escrevem código que descreve como a eletricidade deve fluir através de um circuito. Esse código, conhecido como nível de transferência de registro ou RTL, atua como um projeto para o hardware físico. Durante décadas, criar esse código tem sido um processo meticuloso, impulsionado por humanos, onde cada linha é verificada contra uma referência confiável para garantir que o chip funcionará corretamente. Recentemente, a inteligência artificial começou a escrever esse código para nós. Grandes modelos de linguagem, o mesmo tipo de tecnologia que pode escrever histórias ou responder perguntas, estão agora sendo solicitados a gerar esses complexos projetos de hardware a partir de simples descrições de texto. Embora esses modelos possam produzir muitas versões de um design rapidamente, um problema crítico permanece: como os engenheiros sabem quais desses designs gerados por IA realmente funcionam? No passado, a resposta era comparar a saída da IA contra uma referência perfeita, feita por humanos, ou executá-la através de um teste de simulação. No entanto, criar essas referências perfeitas é caro e demorado, e os próprios testes podem, às vezes, perder erros ocultos.

Uma equipe de pesquisadores da Universidade de Columbia introduziu uma nova maneira de filtrar esses designs gerados por IA sem a necessidade de uma referência perfeita ou de um teste pré-escrito. Eles chamam seu sistema de NoTB. Em vez de depender de um único juiz para decidir se um design é bom, ou de executar uma simulação que pode perder uma falha crítica, o NoTB pede que vários modelos de IA diferentes escrevam o mesmo design de forma independente. Ele então utiliza uma ferramenta matemática rigorosa chamada verificação de equivalência sequencial para ver se as diferentes versões se comportam exatamente da mesma forma sob todas as condições possíveis. A ideia central é que, se vários modelos de IA diferentes, que foram treinados de maneiras distintas, chegarem exatamente ao mesmo comportamento, é altamente provável que tenham encontrado a solução correta. Essa abordagem permite que os engenheiros identifiquem os designs mais confiáveis precocemente no processo, economizando tempo e recursos antes de se comprometerem com a construção do chip real.

Os pesquisadores testaram este método em setenta e oito diferentes tarefas de design de hardware. Eles usaram quatro famílias distintas de grandes modelos de linguagem para gerar múltiplas versões de cada design. Para cada tarefa, eles compararam as saídas para ver quais eram matematicamente idênticas. Eles descobriram que, quando designs de todas as quatro famílias de IA concordavam com o mesmo comportamento, o sistema estava correto quase noventa e cinco por cento das vezes. Esse alto nível de confiança veio com uma compensação: o sistema só fazia uma previsão para cerca de vinte e sete por cento das tarefas. No entanto, ao reduzir o requisito para apenas três famílias concordantes, o sistema pôde cobrir trinta e três por cento das tarefas, mantendo ainda uma taxa de precisão de oitenta e sete por cento. Isso oferece aos designers uma ferramenta flexível: eles podem escolher ser extremamente cautelosos e aceitar apenas os designs mais certos, ou podem aceitar um risco ligeiramente maior para obter mais designs aprovados para testes posteriores.

O estudo também revelou por que os métodos antigos de verificação de designs de IA eram não confiáveis. Uma abordagem comum envolvia pedir a um segundo modelo de IA para atuar como juiz e prever se um design estava correto. Os pesquisadores descobriram que esse método era inconsistente; o mesmo design poderia ser marcado como correto por um juiz e incorreto por outro, dependendo de qual modelo de IA estava realizando a julgamento. Outro método envolvia executar os designs através de um teste criado por uma IA. Os pesquisadores descobriram que a qualidade dos resultados dependia inteiramente da qualidade desse teste. Se o teste fosse fraco, ele poderia falhar em detectar erros, levando o sistema a acreditar que um design falho era, na verdade, correto. Em contraste, o novo método não depende de um teste ou de um juiz. Ele se baseia no fato de que os designs em si são provados como sendo idênticos em todo o intervalo de entradas possíveis, tornando o acordo uma propriedade do design, em vez de uma propriedade da ferramenta usada para verificá-lo.

Para tornar este processo eficiente, o sistema utiliza uma técnica de filtragem inteligente. Em vez de comparar cada par de designs individualmente, o que levaria muito tempo, ele primeiro remove duplicatas exatas e depois agrupa designs que já foram provados como sendo os mesmos. Isso reduz significativamente o número de comparações necessárias. Todo o processo, desde a geração dos designs até a verificação, leva em média entre um e dezesseis minutos por tarefa, dependendo de quantas versões são geradas. O custo de execução deste sistema também é gerenciável, pois evita a necessidade de chamadas caras e repetidas a modelos de IA apenas para atuarem como juízes. Os pesquisadores enfatizam que este método não substitui a necessidade de verificação final. Em vez disso, ele atua como um sistema de triagem, uma forma de organizar a pilha de designs gerados por IA para que os mais promissores possam seguir adiante com confiança, enquanto os incertos são deixados de lado para uma verificação mais tradicional e minuciosa.

As descobertas sugerem que a diversidade dos modelos de IA utilizados é a chave para o sucesso do sistema. Os pesquisadores testaram o que aconteceria se removessem uma das quatro famílias de IA da mistura. Eles descobriram que o sistema permanecia robusto e preciso mesmo quando um modelo estava faltando, provando que o sinal de confiança vem do acordo coletivo do grupo, e não dependendo de um único modelo. Isso torna a abordagem prática para o uso no mundo real, onde o acesso a modelos de IA específicos pode variar. O estudo conclui que, ao mudar o foco de testes simulados para a prova matemática formal de acordo, os engenheiros podem construir um pipeline mais confiável para o uso de inteligência artificial no design de hardware. Isso permite que a indústria aproveite a velocidade da geração por IA enquanto mantém os rigorosos padrões de segurança exigidos pelos complexos chips que alimentam a tecnologia moderna.

Resumo Técnico: NoTB – Triagem de RTL Gerada por LLM sem Dependência de Oráculo via Consenso Formal entre Modelos Cruzados

Definição do Problema
Modelos de Linguagem de Grande Escala (LLMs) são cada vez mais capazes de gerar designs de nível de transferência de registro (RTL) sintetizáveis a partir de especificações em linguagem natural. No entanto, um gargalo crítico permanece: avaliar a correção funcional desses designs gerados precocemente no processo sem acesso a um "oráculo" confiável (como um testbench de referência ou um modelo RTL de ouro). Construir tais oráculos é caro e propenso a erros, sendo frequentemente indisponível no início de uma tarefa de design.

As abordagens existentes sem oráculo sofrem de limitações fundamentais:

LLM-as-a-Judge (LLM como Juiz): Substitui a execução por predição baseada em modelo, mas carece de garantias formais e exibe um forte viés dependente do modelo, levando a taxas de falso-aceite inconsistentes (variando em até 45% entre modelos).
Autoconsistência Baseada em Simulação: Depende do acordo comportamental sob testbenches gerados por LLM. Esta abordagem assume que o testbench cobre o espaço de entrada relevante e que implementações incorretas discordam entre si. Na prática, testbenches fracos podem perder entradas críticas, permitindo que designs incorretos formem um "falso consenso", enquanto modos de erro compartilhados podem fazer com que múltiplos modelos convirjam para o mesmo comportamento errado.

Metodologia: O Framework NoTB
Os autores introduzem o NoTB, um framework que substitui o acordo heurístico por consenso formal entre modelos cruzados. A ideia central é que, se as implementações produzidas por famílias de LLMs treinadas de forma independente forem provadas equivalentes sobre todo o espaço de entrada via Verificação de Equivalência Sequencial (SEC), o acordo entre elas é uma propriedade dos próprios designs, não de um conjunto finito de vetores de teste.

O fluxo de trabalho do NoTB consiste em quatro estágios:

Geração de RTL Multi-Modelo: Para uma determinada especificação, o sistema amostra múltiplas implementações de RTL de $M$ famílias de LLMs treinadas independentemente (ex: Claude, GPT, Gemini, Qwen). Cada modelo gera $K$ candidatos, criando um conjunto de candidatos diversificado $D(s)$ .
Agrupamento de Equivalência Formal: O NoTB constrói um grafo onde os nós são as implementações candidatas e as arestas representam a equivalência provada. Ele utiliza uma ferramenta formal (Cadence JasperGold) para realizar a Verificação de Equivalência Sequencial (SEC) em pares de designs.
- Dois designs são conectados apenas se a ferramenta provar que eles produzem saídas idênticas para todas as sequências de entrada.
- Resultados inconclusivos ou incompatibilidades de interface não criam arestas.
- Componentes conectados neste grafo formam clusters de equivalência.
Poda Incremental: Para gerenciar o custo computacional ( $O(|D|^2)$ $O (∣ D ∣^{2})$ ), o NoTB emprega uma poda leve:
- Arquivos sintaticamente idênticos são mesclados via hashing antes da SEC.
- Uma estrutura de dados union-find rastreia componentes de equivalência; uma vez que um par é provado equivalente, comparações futuras dentro desse componente são ignoradas.
- Não-equivalências provadas entre representantes de componentes impedem verificações redundantes entre componentes.
Pontuação de Confiança via Diversidade de Modelos: O sistema identifica o maior cluster de equivalência ( $C^*$ $C^{*}$ ) para uma especificação. A pontuação de confiança é definida pelo número de modelos: o número de famílias distintas de LLM representadas dentro desse cluster.
- Um número maior de modelos indica que modelos com diferentes vieses indutivos convergiram para o mesmo comportamento formalmente provado.
- Designers podem definir um limiar $\tau$ (ex: $\tau=4$ ) para aceitar apenas especificações onde o cluster dominante contenha implementações de pelo menos $\tau$ famílias distintas. Isso cria um tradeoff ajustável entre precisão (confiança) e cobertura (número de especificações aceitas).

Principais Contribuições

Demonstração da Dependência de Testbench: O artigo mostra que a triagem sem oráculo baseada em simulação é altamente sensível ao gerador de testbench. Em um pool de candidatos fixo, a precisão de um acordo de quatro vias de simulação variou de 43% a 84% baseando-se apenas em qual LLM gerou o testbench.
Introdução do NoTB: Um novo framework que substitui o acordo aprendido/baseado em simulação por consenso formal entre modelos cruzados. Ele agrupa candidatos por SEC e pontua-os pelo diversidade de famílias de LLM no cluster.
Sinal de Correção Calibrado: Evidência empírica de que o número de modelos é um sinal calibrado para correção. O sistema demonstra uma relação monotônica: um acordo formal entre modelos cruzados mais forte correlaciona-se com menores taxas de erro empírico.

Resultados Experimentais
Avaliado em 78 tarefas de geração de RTL do benchmark NVIDIA CVDP usando quatro famílias de LLM (Claude 3.7, GPT-OSS-120B, Gemini 2.5, Qwen 3) com 5 amostras cada:

Consenso de Quatro Famílias ( $\tau=4$ ): Alcançou 94,7% de precisão com 27% de cobertura.
Consenso de Três Famílias ( $\tau=3$ ): Alcançou 87% de precisão com 33% de cobertura.
Comparação com Baselines:
- LLM-as-a-Judge: Mostrou alta instabilidade; as taxas de falso-positivo variaram significativamente dependendo do gerador e do modelo juiz.
- Agrupamento Baseado em Simulação: A precisão flutuou drasticamente (43%–84%) dependendo do gerador de testbench, enquanto a SEC formal permaneceu estável em ~95%.
Robustez: Estudos de ablação leave-one-out confirmaram que o sinal de alta precisão não depende de uma única família de modelos específica; a alta precisão foi mantida mesmo quando uma família era removida.
Custo: Embora a SEC exija um tempo de computação significativo (mediana de 1–16 minutos por especificação dependendo das amostras), ela evita os custos massivos de tokens associados à execução de milhares de chamadas de "juiz" ou à geração de múltiplos testbenches para cada candidato.

Significância e Alegações
O artigo afirma que o NoTB fornece uma base confiável e sem oráculo para triagem de alta confiança nos estágios iniciais do design de hardware. Ao alavancar garantias formais em vez de heurísticas aprendidas ou vetores de teste finitos, o NoTB permite que designers certifiquem seletivamente um subconjunto de designs de RTL gerados que provavelmente estão corretos, permitindo que ignorem verificações de estágio inicial ou os priorizem para verificação final. Os autores enfatizam que o NoTB não substitui a necessidade de um oráculo de confiança ou de um fluxo de verificação completo; em vez disso, ele atua como um filtro para identificar candidatos de alta confiança antes que uma referência de ouro esteja disponível. O método é apresentado como uma solução prática para o problema da "triagem", oferecendo controle explícito sobre o tradeoff risco–cobertura sem exigir oráculos dependentes de modelos.

Mais como este