🤖 AI

NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

Este artigo apresenta o NeuroAbs, um framework neuro-simbólico que utiliza LLMs para identificação de sinais RTL e representação simbólica baseada em AST, combinados com verificação de correção baseada em SMT e refinamento CEGAR, para automatizar a abstração de RTL e acelerar significativamente a verificação de propriedades de hardware.

Autores originais: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

Publicado 2026-08-19

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

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 oculto da eletrônica moderna, os chips que alimentam nossos telefones, carros e computadores são construídos a partir de bilhões de minúsculos interruptores. Antes que esses chips sejam sequer fabricados, os engenheiros devem provar que eles se comportarão exatamente como pretendido, não importa quais instruções recebam. Esse processo, conhecido como verificação formal, é uma checagem matemática rigorosa que garante que um projeto esteja livre de falhas ocultas. No entanto, à medida que esses projetos se tornam mais complexos, a tarefa de verificá-los torna-se esmagadora. O número absoluto de estados possíveis em que um chip pode entrar é tão vasto que até mesmo os computadores mais poderosos lutam para explorá-los todos em um tempo razoável. Para resolver isso, os engenheiros frequentemente utilizam uma técnica chamada abstração, que simplifica um projeto complexo removendo detalhes que não importam para um teste específico, de forma muito semelhante a olhar para o mapa de uma cidade que mostra apenas as estradas principais necessárias para uma viagem específica, ignorando todas as ruas secundárias e vielas.

Durante anos, a criação desses modelos simplificados exigiu ou o trabalho manual tedioso de especialistas humanos ou dependeu de regras rígidas e pré-programadas que frequentemente perdiam as nuances de um projeto específico. Uma nova abordagem chamada NeuroAbs oferece um caminho diferente, combinando a força de reconhecimento de padrões da inteligência artificial com a lógica estrita da matemática formal. Este método utiliza modelos de linguagem de grande escala — sistemas de IA avançados treinados em vastas quantidades de texto — para compreender a intenção por trás de um projeto de hardware e uma propriedade específica que ele precisa satisfazer. A IA identifica quais partes do circuito são irrelevantes para o teste atual e sugere como simplificá-las. No entanto, como a IA pode às vezes cometer erros ou sugerir mudanças que quebram a lógica, o sistema não confia na IA cegamente. Em vez disso, ele atua como uma estrutura neuro-simbólica, onde a IA propõe mudanças e um motor matemático separado e rigoroso verifica imediatamente se essas mudanças são seguras. Se a simplificação for agressiva demais e correr o risco de esconder um erro real, o sistema refina automaticamente o modelo, removendo as camadas de simplificação apenas o suficiente para restaurar a precisão sem perder os benefícios de velocidade.

Os pesquisadores por trás do NeuroAbs testaram sua estrutura em vários projetos de processadores do mundo real e componentes periféricos, incluindo uma interface de comunicação comum usada em muitos dispositivos. Eles descobriram que o sistema conseguia identificar com sucesso oportunidades para simplificar a lógica que os métodos tradicionais baseados em regras não detectavam. Por exemplo, ao verificar uma instrução específica em um processador, a IA percebeu que a lógica que lidava com outras instruções não relacionadas poderia ser substituída com segurança por um marcador genérico. Isso permitiu que o mecanismo de verificação focasse apenas nas partes relevantes do circuito. Em experimentos, essa abordagem acelerou significamente o tempo necessário para provar que um projeto estava correto. Quando os pesquisadores integraram o NeuroAbs com ferramentas de verificação de alto desempenho já existentes, o tempo necessário para alcançar uma prova formal caiu quase pela metade em muitos casos. Mesmo quando uma prova completa não era possível dentro do limite de tempo, os modelos simplificados permitiram que o sistema explorasse muito mais profundamente o comportamento do circuito, descobrindo possíveis bugs que permaneceriam ocultos de outra forma.

O sucesso deste método depende de um equilíbrio cuidadoso entre a flexibilidade da IA e a precisão da lógica formal. O sistema primeiro analisa o projeto e o cenário de teste específico para identificar quais sinais são críticos. Ele então usa a IA para reescrever o código nessas áreas específicas, substituindo cálculos complexos por valores abstratos mais simples. Crucialmente, cada reescrita é submetida a uma verificação matemática estrita para garantir que não altere o comportamento fundamental do chip de uma forma que invalide o teste. Se a verificação falhar, o sistema utiliza um ciclo de feedback para identificar exatamente qual simplificação causou o problema e reverte essa parte específica à sua forma original. Esse processo iterativo garante que o modelo final seja simples o suficiente para ser verificado rapidamente e preciso o suficiente para ser confiável. Os resultados mostram que esta abordagem híbrida pode lidar com diversos tipos de lógica de hardware, desde operações aritméticas simples até estruturas de ramificação complexas, tornando-se uma ferramenta poderosa para a próxima geração de design de chips.

Ao automatizar a criação desses modelos simplificados, o NeuroAbs aborda um grande gargalo na engenharia de hardware. Anteriormente, a decisão sobre o que simplificar e como fazê-lo dependia fortemente da intuição humana ou de regras fixas que não podiam se adaptar a cada desafio de design único. Esta nova estrutura demonstra que a inteligência artificial pode ser efetivamente guiada para realizar essas tarefas, desde que ancorada por um sistema que verifique cada etapa. As descobertas sugerem que o futuro da verificação de hardware pode residir em sistemas colaborativos como este, onde as máquinas lidam com o trabalho pesado de reconhecimento de padrões e sugestões, enquanto o rigor matemático garante a segurança e a correção do produto final. À medida que os designs de chips continuam a crescer em complexidade, ferramentas como o NeuroAbs oferecem uma maneira promissora de acompanhar o ritmo, garantindo que os dispositivos em que confiamos sejam construídos sobre uma base de verdade verificada.

Resumo Técnico: NeuroAbs

Declaração do Problema

A verificação formal, especificamente a verificação de propriedades (model checking), é essencial para garantir a correção funcional de designs de hardware. No entanto, à medida que os designs de Register-Transfer-Level (RTL) crescem em tamanho e complexidade, provar propriedades especificadas pelo usuário de forma eficiente torna-se um gargalo significativo. Embora técnicas de abstração sejam comumente usadas para reduzir a complexidade do sistema ao substituir modelos concretos por representações simplificadas, os métodos existentes enfrentam duas limitações primárias:

Abstração Manual: Depende fortemente da percepção humana e é intensiva em mão de obra, exigindo que engenheiros identifiquem manualmente quais partes do design são irrelevantes para uma propriedade específica.
Abstração Automática Baseada em Regras: Técnicas como abstração estrutural, abstração guiada por sintaxe e abstração de datapath (por exemplo, substituir aritmética por funções não interpretadas) carecem de flexibilidade. Elas frequentemente falham em identificar oportunidades de abstração que dependem da intenção semântica específica de um cenário de verificação e da propriedade alvo, pois baseiam-se em regras sintáticas predefinidas em vez de compreensão funcional.

Consequentemente, os métodos atuais frequentemente perdem oportunidades de abstrair com segurança a lógica que é irrelevante para um objetivo de verificação específico, ou produzem abstrações que são ou muito grosseiras (levando a contraexemplos espúrios) ou muito conservadoras (falhando em acelerar a verificação).

Metodologia: O Framework NeuroAbs

O artigo propõe o NeuroAbs, um framework neuro-simbólico que integra Grandes Modelos de Linguagem (LLMs) com raciocínio simbólico para automatizar a abstração de RTL. O framework opera em três estágios distintos:

1. Análise de Sinais Assistida por LLM (Componente Neural)

Em vez de alimentar bases de código RTL inteiras para um LLM, o que excede os limites de contexto, o NeuroAbs emprega um Analisador de Sinais para identificar sinais candidatos para abstração.

Entrada: Especificações do design, descrições de cenários de verificação e definições de sinais.
Processo: Usando prompting de Cadeia de Pensamento (Chain-of-Thought - CoT) e instruções de sistema customizadas, o LLM analisa o cenário de verificação para identificar "sinais relacionados ao cenário". Ele determina quais sinais controlam a lógica relevante para a propriedade específica e sugere valores fixos (por exemplo, definir um opcode para um tipo de instrução específico).
Integração de Análise Estática: A saída do LLM é combinada com a análise estática de RTL (por exemplo, propagação de constantes) para localizar as regiões de código específicas e as instruções afetadas por esses sinais. Isso estreita o escopo de todo o design para um pequeno conjunto de instruções candidatas.

2. Abstração Guiada por AST (Núcleo Neuro-Simbólico)

Para garantir a integridade estrutural e evitar que o LLM reescreva a lógica não relacionada, o NeuroAbs converte o RTL em uma Árvore de Sintaxe Abstrata (AST).

Localização: O sistema mapeia os sinais candidatos identificados para nós de instrução específicos da AST e seus contextos estruturais envolventes (por exemplo, blocos always, instruções case).
Transformação: Um segundo LLM, o Abstractor, tem a tarefa de reescrever apenas os nós localizados da AST. Ele utiliza aprendizado de poucos disparos (few-shot learning, fornecendo exemplos de instruções originais vs. abstraídas) para gerar abstrações candidatas.
Restrição: O LLM é restrito a reescrever apenas as partes específicas de uma instrução consideradas irrelevantes para a propriedade (por exemplo, substituindo uma operação AND por um valor desconhecido X se a propriedade diz respeito apenas a operações ADD), preservando a lógica relevante.

3. Validação Simbólica e Refinamento (Componente Simbólico)

Cada abstração gerada é rigorosamente validada para garantir que seja uma sobre-aproximação segura do design original.

Verificação SMT: O framework utiliza solvers de Satisfatibilidade Modulo Theories (SMT) (especificamente o Z3) para verificar a condição $\forall V, S(V) \implies \hat{S}(V)$ $\forall V, S (V) ⟹ \hat{S} (V)$ . Isso garante que todo comportamento permitido pela instrução abstrata também é permitido pela original.
- Tratamento de valores X: Como os solvers SMT não suportam nativamente valores desconhecidos (X), estes são traduzidos em variáveis novas vinculadas por quantificadores existenciais ( $\exists Y$ ) para permitir que o solver os trate como escolhas não determinísticas.
Loop CEGAR Customizado (R-CEGAR): Se o modelo abstrato falha em provar a propriedade e gera um contraexemplo, o sistema verifica se o contraexemplo é espúrio.
- Se for espúrio, uma técnica de redução de contraexemplo é aplicada para generalizar o traço e localizar exatamente qual instrução abstraída desencadeou a violação.
- O sistema então reverte apenas as instruções específicas inválidas para sua forma original, em vez de descartar toda a abstração, e itera o processo.

Principais Contribuições

Primeira Aplicação de LLMs à Abstração de RTL: O artigo apresenta o NeuroAbs como o primeiro framework a utilizar LLMs para identificar e gerar abstrações de RTL, indo além das abordagens estáticas baseadas em regras.
Fluxo de Trabalho Neuro-Simbólico: Propõe um fluxo inovador onde o componente neural (LLM) propõe candidatos conscientes do cenário, enquanto o componente simbólico (travessia de AST e SMT) restringe a reescrita a alvos estruturais precisos e valida a correção.
Refinamento Customizado (R-CEGAR): Os autores introduzem um loop de refinamento que utiliza a redução de contraexemplo para identificar e reverter eficientmente apenas as instruções abstratas específicas que causam contraexemplos espúrios, minimizando o número de iterações necessárias.

Resultados Experimentais

O framework foi avaliado em um conjunto de benchmarks incluindo núcleos de processadores RISC-V (PicoRV32, Piccolo, Flute) e um periférico I2C, cobrindo 55 cenários de verificação. Os resultados foram comparados com model checkers de última geração (AVR e RIC3) que já incluem mecanismos de abstração avançados.

Aceleração de Prova Formal: Quando integrado ao AVR, o NeuroAbs reduziu o tempo médio de execução para a construção de provas formais em 44,89%. Mesmo com as capacidades de abstração existentes do AVR, o NeuroAbs proporcionou acelerações adicionais significativas.
Eficiência na Busca de Bugs (BMC): Para casos em que as provas formais não puderam ser concluídas dentro do limite de tempo, o NeuroAbs acelerou significativamente o processo de Bounded Model Checking (BMC).
- No caso "Piccolo", a profundidade média de desdobramento (unrolling depth) aumentou de 109,36 para 125,36 ciclos.
- No caso "Flute", o tempo necessário para atingir a profundidade máxima do baseline foi reduzido em 75,98%.
Estudos de Ablação: Experimentos confirmaram que tanto o aprendizado de poucos disparos (few-shot learning) quanto as instruções customizadas são críticos. Remover o aprendizado de poucos disparos reduziu a taxa de sobre-aproximação de 95,27% para 83,51%. Remover as instruções customizadas causou uma queda de 98,38% nas sobre-aproximações "estritas" (significando que o modelo tendia a reproduzir as instruções originais em vez de abstraí-las).
Redução de Complexidade: A análise dos circuitos And-Inverter-Gate (AIG) resultantes mostrou uma redução substancial no índice máximo de variáveis, confirmando que o NeuroAbs simplifica efetivamente a estrutura do circuito.

Significância e Alegações

O artigo afirma que o NeuroAbs aborda a rigidez das abstrações tradicionais baseadas em regras e a intensidade de mão de obra dos métodos manuais. Ao combinar as capacidades de raciocínio semântico de LLMs com o rigor da verificação simbólica, o NeuroAbs pode identificar oportunidades de abstração conscientes do contexto que as regras estáticas não captam.

Os autores posicionam o NeuroAbs não como um substituto para os model checkers existentes, mas como um framework complementar que aumenta sua eficiência. Os resultados demonstram que, mesmo quando integrado a model checkers altamente otimizados e vencedores de competições (AVR e RIC3), a abordagem neuro-simbólica produz melhorias mensuráveis tanto na velocidade de construção de provas quanto na profundidade de busca de bugs. O framework é apresentado como um passo em direção a uma verificação de hardware mais automatizada e consciente de cenários, que reduz a dependência de intervenção manual de especialistas.