FormalRTL: Verified RTL Synthesis at Scale

O artigo apresenta o FormalRTL, um novo framework multiagente que integra modelos de referência de software como especificações formais para gerar e verificar código RTL de forma escalável e confiável, superando os desafios de síntese de hardware em escala industrial.

O essencial

Imagine que você precisa construir uma fábrica de chips extremamente complexa (como os usados em inteligência artificial), mas em vez de desenhar os planos manualmente, você pede ajuda a um assistente de IA super inteligente. O problema é que, se você apenas der uma instrução vaga como "faça um chip que some números", a IA pode criar algo que parece funcionar, mas que na verdade tem falhas graves e não segue as regras exatas da engenharia.

O artigo "FormalRTL" apresenta uma nova solução para esse problema, funcionando como um sistema de construção com "plano mestre" e "inspetor de qualidade".

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

1. O Problema: O Arquiteto que "Adivinha"

Antes, as IAs tentavam escrever o código do chip (chamado RTL) apenas lendo uma descrição em linguagem natural (como "faça uma calculadora").

• A analogia: É como pedir a um pintor: "Pinte um céu azul". Ele pinta, mas talvez use o azul errado, esqueça das nuvens ou pinte o chão de azul também. Em chips, isso é catastrófico. Se o chip errar um cálculo, ele queima ou falha.
• O desafio: Chips industriais são gigantes (milhares de linhas de código) e têm lógicas matemáticas muito difíceis. A IA sozinha não consegue garantir que o resultado final seja 100% correto.

2. A Solução: O "Duplo de Segurança" (FormalRTL)

Os autores criaram o FormalRTL, que não deixa a IA trabalhar sozinha. Eles introduzem um modelo de referência em software (um código em C/C++ que já funciona perfeitamente e é conhecido como "a verdade absoluta").

Pense nisso como uma receita de bolo perfeita (o modelo C) que você usa para guiar a IA na construção do bolo real (o chip).

O sistema funciona com uma equipe de "agentes" (robôs virtuais) que trabalham juntos:

A. O Planejador (O Chefe de Obra)

• O que faz: Em vez de tentar construir o chip inteiro de uma vez, ele olha para a "receita perfeita" (o código C) e a divide em tarefas menores e gerenciáveis.
• A analogia: Imagine que você precisa construir um arranha-céu. O Planejador não diz "construa o prédio". Ele diz: "Primeiro, faça o alicerce. Depois, o 1º andar. Depois, o 2º". Ele usa o código C para saber exatamente quais peças dependem de quais outras, garantindo que nada seja esquecido.

B. O Construtor Inicial (O Pedreiro Rápido)

• O que faz: Ele pega cada pequena tarefa e escreve o código do chip (RTL) tentando imitar a "receita perfeita".
• A analogia: Ele constrói o 1º andar do prédio. Mas, como é uma IA, ele pode cometer erros de alvenaria ou usar o cimento errado.

C. O Inspetor de Qualidade (O Detetive Matemático)

• O que faz: Aqui está a mágica. Em vez de apenas testar o chip com alguns exemplos (o que pode deixar passar erros), o sistema usa uma ferramenta chamada Equivalência Formal.
• A analogia: Imagine um inspetor que não apenas "prova" o bolo, mas usa uma balança de precisão atômica para comparar cada grama do bolo que a IA fez com a receita perfeita.
  • Se houver uma diferença de 0,0001%, o inspetor não diz apenas "está errado". Ele aponta exatamente onde está o erro e diz: "Você usou farinha em vez de açúcar na camada 3".
  • Isso gera um contra-exemplo (um relatório de erro detalhado).

D. O Agente de Depuração (O Mecânico)

• O que faz: Ele pega o relatório do inspetor, entende onde está o erro e pede para a IA corrigir o código.
• A analogia: É como um mecânico que recebe um mapa de erro do carro e conserta a peça específica, em vez de tentar trocar o motor todo de novo. Esse ciclo (Construir -> Inspeccionar -> Corrigir) se repete até que o chip seja idêntico à receita perfeita.

3. Por que isso é revolucionário?

• Escala: Antes, as IAs conseguiam fazer apenas circuitos simples (como uma calculadora básica). O FormalRTL conseguiu construir chips complexos com mais de 1.000 linhas de código, algo que parecia impossível de ser feito automaticamente com segurança.
• Confiança: O sistema não "acha" que está certo. Ele prova matematicamente que o chip faz exatamente o que a receita diz.
• Velocidade: Embora a IA cometa erros no início, o sistema de correção automática é muito mais rápido do que um engenheiro humano tentando achar um erro em milhares de linhas de código.

4. O Resultado Final

Os pesquisadores testaram isso com designs industriais reais (como chips de IA da Huawei e da Ascend).

• O que eles descobriram: O sistema conseguiu gerar chips complexos com sucesso na maioria dos casos.
• A única "desvantagem": O chip gerado automaticamente pode ser um pouco maior ou mais lento do que um chip feito por um engenheiro humano de elite (que otimiza cada detalhe).
• Mas o ganho é: Ter um chip que funciona perfeitamente e serve como uma base sólida. Depois que o chip está "correto", os engenheiros humanos podem pegá-lo e otimizá-lo para ficar mais rápido e menor. É muito mais fácil melhorar algo que já funciona do que tentar consertar algo que não funciona.

Resumo em uma frase

O FormalRTL é como ter um engenheiro-chefe (IA) que constrói chips seguindo uma receita infalível (código C), com um inspetor matemático que garante que nada saia do lugar, permitindo que a indústria de chips crie designs complexos de forma rápida e sem erros.

Resumo técnico

Resumo Técnico: FormalRTL – Síntese RTL Verificada Formalmente em Escala

1. O Problema

O design de chips computacionais intensivos (como GPUs, NPUs e TPUs) tornou-se um gargalo de engenharia devido à complexidade lógica e à busca incessante por metas de Potência, Desempenho e Área (PPA). Embora os Modelos de Linguagem Grandes (LLMs) demonstrem potencial na geração de código, sua aplicação em designs industriais de grande escala enfrenta duas barreiras fundamentais:

1. Complexidade de Design em Grande Escala: Especificações em linguagem natural são frequentemente ambíguas e insuficientes para guiar LLMs na tomada de decisões arquitetônicas complexas para IP (Propriedade Intelectual) industrial, que exigem milhares de linhas de código.
2. Estruturas Aritméticas e Lógicas Intrincadas: Diferente de benchmarks simples, os IPs industriais possuem datapaths profundamente aninhados e tipos de dados personalizados (ex: bfloat16, hifloat8). A verificação baseada apenas em simulação falha em cobrir casos extremos (corner cases), e a síntese direta de RTL a partir de texto não oferece garantias formais de correção.

A lacuna crítica é a falta de uma metodologia que utilize modelos de referência de software (C/C++) como especificações formais executáveis para guiar a síntese e a verificação, uma prática padrão na indústria que os métodos anteriores baseados em LLM ignoraram.

2. Metodologia: FormalRTL

O FormalRTL é um framework end-to-end baseado em agentes múltiplos que integra modelos de referência de software para guiar a geração e verificação de código RTL (Register-Transfer Level). O fluxo de trabalho é composto por três agentes principais:

• Agente de Planejamento (Planning Agent):

  • Realiza análise estática no modelo de referência em C (usando a Árvore de Sintaxe Abstrata - AST) para decompor o design complexo em sub-tarefas modulares.
  • Refatora a especificação principal em especificações-alvo para cada submódulo, seguindo a ordem topológica das dependências de função.
  • Isso mitiga ambiguidades arquitetônicas e limita o escopo da verificação formal a uma escala gerenciável.

• Agente de Inicialização (Initializing Agent):

  • Gera o código RTL inicial e um harness de verificação para cada submódulo, ancorado diretamente no modelo de referência C.
  • O harness assume entradas idênticas e asserta a equivalência de saída entre o software e o hardware.
  • Determina o tempo de execução (número de ciclos de relógio) necessário, alinhando estágios de pipeline com requisitos de latência para suportar verificação de equivalência transacional.

• Agente de Depuração (Debugging Agent):

  • Utiliza ferramentas de Verificação de Equivalência (EC) formais (hw-cbmc) para comparar o modelo C e o RTL.
  • Recebe dois tipos de feedback: erros de sintaxe e contraexemplos (quando a equivalência falha).
  • Emprega um Localizador de Bugs para identificar linhas de erro e um Simplificador de Contraexemplos para reduzir relatórios complexos, mostrando apenas as funções problemáticas e sinais incompatíveis.
  • O LLM utiliza essas informações refinadas para gerar patches de código, fechando o ciclo de depuração automática.

3. Contribuições Principais

1. Metodologia Orientada a Modelo de Referência: Pioneira na utilização de modelos de software (C/C++) como especificações formais executáveis para guiar a síntese de hardware ágil, garantindo escalabilidade e correção.
2. Motor Multi-Agente End-to-End: Desenvolvimento de um pipeline automatizado que integra planejamento, síntese, depuração e verificação formal, eliminando a necessidade de testbenches manuais extensivos.
3. Benchmarks Industriais de Nova Geração: Criação e liberação de um conjunto de benchmarks de nível industrial (incluindo operadores FP16 e tipos de dados Hifloat8), fornecendo especificações e modelos de referência de software para cada caso, preenchendo uma lacuna na pesquisa atual.

4. Resultados Experimentais

Os experimentos foram realizados em uma suíte de benchmarks complexos (incluindo casos acadêmicos do repositório "softfloat" e casos industriais baseados no chip Ascend AI).

• Desempenho em Nível de Módulo:

  • O sistema alcançou altas taxas de sucesso final (FSR), mesmo em módulos com mais de 1.000 linhas de código.
  • A taxa de sucesso inicial (ISR) foi baixa para muitos módulos (indicando a dificuldade dos LLMs em gerar código perfeito na primeira tentativa), mas o agente de depuração corrigiu a maioria dos erros, elevando a FSR para 95-100% na maioria dos casos.
  • A estratégia de verificação "bottom-up" (verificar dependências antes do módulo superior) provou ser altamente eficaz, resultando em maior estabilidade para módulos de topo.

• Estudo de Ablação (Planejamento):

  • Comparado a uma linha de base que usa apenas especificação em linguagem natural (sem análise de código C), o FormalRTL demonstrou superioridade significativa em designs maiores.
  • Enquanto a linha de base falhou completamente (0% de sucesso) em designs complexos devido à sobrecarga de gerenciamento de estado, o FormalRTL manteve alta estabilidade e escalabilidade.

• Estudo de Ablação (Depuração):

  • A remoção de componentes como o "Simplificador de Contraexemplos" ou a "Depuração Guiada por Contraexemplos" resultou em um aumento drástico no número de iterações necessárias e uma queda significativa na taxa de sucesso final, comprovando a eficácia do feedback formal.

• Qualidade do Resultado (QoR):

  • Os designs gerados pelo FormalRTL apresentaram áreas e atrasos ligeiramente superiores aos designs otimizados manualmente por engenheiros. No entanto, o artigo enfatiza que o valor principal é a correção funcional garantida, fornecendo uma base executável confiável para iterações subsequentes de otimização PPA.

5. Significado e Impacto

O FormalRTL representa um avanço crucial ao fechar a lacuna entre prototipagem baseada em LLM e o desenvolvimento de hardware real. Ao integrar modelos de referência de software e verificação formal no ciclo de geração de código, o framework oferece:

• Garantias Formais: Assegura que a implementação RTL é funcionalmente equivalente à especificação de software, algo que métodos puramente baseados em simulação não conseguem garantir.
• Escalabilidade Industrial: Demonstra a viabilidade de gerar e verificar designs de datapath complexos e de grande escala, superando as limitações de ambiguidade e cobertura de testes.
• Aceleração do Fluxo de Design: Reduz o esforço de engenharia na criação de testbenches e na depuração manual, permitindo um desenvolvimento de hardware mais ágil e confiável.

O trabalho sugere que o futuro da síntese de hardware assistida por IA depende da integração profunda com especificações formais e ferramentas de verificação, em vez de depender exclusivamente da capacidade de geração de texto dos LLMs.