Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

Este artigo apresenta uma metodologia escalável para verificação formal de aritmética de ponto flutuante em nível RTL, que utiliza uma estratégia de dividir e conquistar com refinamento guiado por contraexemplos e geração automatizada de propriedades por IA para superar as limitações dos modelos de alto nível e alcançar maior eficiência de cobertura.

O essencial

Imagine que você está construindo uma ponte extremamente complexa e precisa. Se um único parafuso estiver torto ou se o cálculo de peso estiver errado, a ponte pode desmoronar. No mundo dos computadores, essa "ponte" é o circuito que faz contas com números decimais (como 3.14 ou 0.0001), chamado de Unidade de Ponto Flutuante (FPU).

Este artigo apresenta uma nova maneira de garantir que essa "ponte" esteja perfeita antes de ser usada, usando uma combinação de lógica matemática rigorosa e inteligência artificial.

Aqui está a explicação passo a passo, usando analogias do dia a dia:

1. O Problema: Traduzir para o Idioma Errado

Antes, para verificar se um chip de computador estava funcionando bem, os engenheiros faziam algo como:

• Pegavam o projeto final (escrito em uma linguagem de hardware complexa chamada RTL).
• Tentavam traduzir esse projeto para uma linguagem de software (C++), como se tentassem traduzir um poema de português para inglês e depois para japonês.
• Comparavam o resultado.

O problema: Nessa tradução, coisas importantes se perdem (como se você traduzisse "amor" e o resultado fosse apenas "sentimento forte"). Além disso, a tradução demorava muito e podia conter erros de interpretação.

2. A Solução: O "Espelho Perfeito" (Verificação RTL-a-RTL)

Os autores propõem uma abordagem mais direta: não traduzir nada.

• Imagine que você tem duas cópias idênticas de um desenho de arquitetura.
• Uma cópia é o Projeto Dourado (a referência perfeita, feita manualmente para garantir que está certo).
• A outra é o Projeto Real (o que os engenheiros estão construindo de verdade).
• Em vez de traduzir, eles colocam os dois projetos lado a lado, bloco por bloco, e usam um "robô matemático" (ferramenta de verificação formal) para garantir que, para cada entrada, a saída seja exatamente a mesma nas duas cópias.

3. A Estratégia: Quebrar o Elefante em Fatias

Verificar todo o chip de uma vez é como tentar comer um elefante inteiro de uma só vez: impossível e confuso.

• Divisão em Estágios: Eles dividiram a conta matemática em etapas menores (como alinhar os números, somar e arredondar).
• Teoremas e "Provas de Conceito": Eles criaram regras pequenas (lemas) para cada etapa. Se a etapa 1 estiver certa e a etapa 2 estiver certa, então o resultado final está certo.
• O "Detetive de Erros": Se algo não bate, a ferramenta gera um CEX (um contra-exemplo). É como se um detetive dissesse: "Ei, quando você colocou o número 5 e 3, o resultado deu 9 em vez de 8. Olhe aqui exatamente onde o erro aconteceu." Os engenheiros consertam o erro e testam de novo.

4. O Toque Moderno: A Inteligência Artificial como Estagiário Criativo

Aqui entra a parte mais inovadora: usar Inteligência Artificial (IA) para ajudar a escrever as regras de verificação.

• O Estagiário (IA): Eles pediram para IAs (como GPT-5 e Llama) lerem o projeto e escreverem as regras de verificação (os "asserts").
• O Chefe (Humano): A IA é inteligente, mas às vezes alucina ou escreve regras redundantes (repetitivas). Por isso, um humano (o "Human-in-the-Loop") revisa o trabalho da IA.
• O Resultado: A IA gera um rascunho rápido, e o humano refina. Juntos, eles criam um conjunto de regras muito eficiente.

5. O Teste de Estresse: "Injeção de Falhas"

Para ter certeza de que o sistema de verificação funciona, eles fizeram algo maluco: quebraram o projeto de propósito.

• Eles introduziram erros intencionais no código (como mudar um sinal de mais para menos ou errar um arredondamento).
• O sistema de verificação conseguiu detectar todos esses erros, provando que a "ponte" de segurança é forte o suficiente para pegar qualquer falha.

6. Os Resultados: O Que Descobriram?

• Sem IA: Fazer tudo manualmente é preciso, mas demorado.
• IA sozinha: A IA gera muitas regras, mas muitas são repetidas ou não cobrem tudo.
• IA + Humano (O Pulo do Gato): Quando a IA gera as regras e o humano as ajusta, o sistema fica rápido, preciso e cobre quase 100% do que precisa.
• Comparação: Verificar o projeto contra o "Projeto Dourado" (RTL-a-RTL) foi muito mais eficiente do que tentar verificar o projeto sozinho sem uma referência perfeita.

Resumo Final

Este paper diz: "Pare de traduzir projetos de hardware para software e perder tempo. Use uma ferramenta matemática para comparar o projeto real com um modelo perfeito, peça para a IA ajudar a escrever as regras de teste, mas deixe um humano supervisionar. Assim, você encontra erros complexos mais rápido e com mais confiança."

É como ter um engenheiro sênior (o modelo dourado), um estagiário super-rápido (a IA) e um inspetor de qualidade (o humano) trabalhando juntos para garantir que a ponte nunca caia.

Resumo técnico

Resumo Técnico: Verificação Formal de Aritmética de Ponto Flutuante

1. O Problema

A verificação formal de unidades de ponto flutuante (FPUs) é um dos desafios mais complexos no projeto de hardware moderno devido a:

• Comportamento Não Linear: A natureza da aritmética de ponto flutuante (IEEE-754) envolve operações não lineares como alinhamento de expoentes, normalização e arredondamento.
• Acoplamento Controle-Datapath: A interação estrita entre a lógica de controle (tratamento de exceções) e os caminhos de dados aritméticos torna a exploração exaustiva do estado difícil.
• Limitações das Abordagens Atuais: Métodos existentes frequentemente dependem de modelos de alto nível em C para verificação de equivalência contra o RTL (Register Transfer Level). Isso introduz:
  • Lacunas de abstração entre o modelo C e a implementação de hardware.
  • Sobrecarga de tradução e manutenção.
  • Escalabilidade limitada para designs RTL densos em datapath.

2. Metodologia Proposta

O artigo apresenta uma metodologia escalável de verificação direta RTL-a-RTL (RTL-to-RTL), eliminando a dependência de modelos de software (C/C++). A abordagem baseia-se nos seguintes pilares:

• Model Checking Direto: Comparação exata entre a implementação RTL e um modelo de referência "golden" (também em RTL/SystemVerilog), garantindo precisão bit-a-bit sem abstração.
• Estratégia "Divide-and-Conquer" (Dividir para Conquistar):
  • O design (um somador de ponto flutuante) é decomposto hierarquicamente em estágios modulares: Estágio de Alinhamento de Mantissa e Estágio de Adição e Arredondamento.
  • A prova de corretude é estruturada como um teorema principal apoiado por lemas intermediários e assertions (propriedades) de nível de estágio.
  • Isso reduz o "cone de influência" (COI), diminuindo a complexidade da prova e facilitando o debug.
• Refinamento Guiado por Contraexemplo (CEX): Quando o verificador formal encontra uma discrepância, o CEX é usado para isolar o defeito, refinar a implementação ou ajustar as propriedades, até que a equivalência seja provada.
• Geração de Propriedades com IA Agente:
  • Utilização de um sistema multi-agente baseado em LLMs (como GPT-5, Llama3.3) para gerar automaticamente SystemVerilog Assertions (SVAs) a partir de especificações em linguagem natural.
  • Integração de Human-in-the-Loop (HITL): Um ciclo iterativo onde um especialista humano refina as propriedades geradas pela IA, corrigindo ambiguidades e garantindo a aderência à intenção de design.

3. Contribuições Principais

1. Verificação RTL-a-RTL Pura: Eliminação de modelos de referência em C, permitindo verificação direta e precisa em nível de RTL.
2. Decomposição Hierárquica: Uso de lemas e assertions modulares para provar a corretude de estágios complexos de forma isolada, melhorando a convergência da prova.
3. Detecção de Bugs e Prova Formal: Identificação e correção de defeitos de implementação (ex: seleção incorreta de operandos, lógica de inversão falha) e prova formal de equivalência funcional.
4. Injeção de Falhas: Validação da robustez do processo de verificação através da injeção sistemática de falhas no datapath para garantir que as propriedades consigam detectar erros críticos de precisão.
5. Análise de Cobertura com IA: Comparação entre propriedades escritas manualmente e geradas por IA, demonstrando que a IA, quando guiada por HITL, pode alcançar eficiência superior com menos assertions.

4. Resultados e Avaliação

Os experimentos foram realizados na plataforma Cadence Jasper Formal Verification em um somador de ponto flutuante de precisão simples (open-source).

• Detecção de Defeitos: O fluxo identificou e corrigiu bugs reais na implementação, como seleção incorreta de operandos quando os expoentes eram iguais e erros de lógica de inversão durante subtrações.
• Eficácia da IA (Geração de Propriedades):
  • Com Modelo de Referência (RTL-a-RTL): As propriedades geradas por IA (após refinamento HITL) alcançaram cobertura formal de 98,42% (comparável às manuais) usando apenas 3 a 6 assertions, enquanto as versões iniciais sem HITL exigiam 7 a 15 assertions com redundância.
  • Sem Modelo de Referência (Standalone RTL): A cobertura caiu significativamente (para ~62-90%) devido à dificuldade da IA em restringir o espaço de estados válido sem orientação micro-arquitetural. O refinamento HITL foi crucial para aumentar a cobertura, mas exigiu muito mais esforço humano.
• Eficiência: A abordagem RTL-a-RTL com IA refinada por HITL provou ser mais eficiente em tempo de prova e número de assertions do que a verificação standalone.
• Injeção de Falhas: Todas as falhas injetadas (ex: distorção de sticky-bit, erro de normalização, violação de regras de arredondamento) foram detectadas com sucesso pelas propriedades formais.

5. Significado e Conclusão

Este trabalho estabelece um novo paradigma para a verificação de datapaths aritméticos complexos:

• Precisão: Ao remover a camada de abstração C, elimina-se o risco de discrepâncias semânticas entre o modelo de especificação e o hardware real.
• Escalabilidade com IA: Demonstra que a Inteligência Artificial Generativa pode acelerar a criação de propriedades formais, mas requer supervisão humana (HITL) para ser eficaz, especialmente em designs complexos onde a intenção micro-arquitetural é crítica.
• Futuro: A metodologia serve como base para a verificação de unidades mais complexas (multiplicadores, divisores) e sugere que o futuro da verificação formal reside na simbiose entre a exaustividade matemática dos verificadores formais e a capacidade de síntese de LLMs, mediada por especialistas humanos.

Em suma, o artigo prova que a verificação formal direta RTL-a-RTL, potencializada por agentes de IA e refinada por humanos, oferece uma estratégia superior, mais robusta e escalável para garantir a corretude de hardware de ponto flutuante em comparação com métodos tradicionais baseados em C.