💬 NLP

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

CktFormalizer é um framework que aproveita a linguagem de descrição de hardware (HDL) com tipos dependentes do Lean 4 para orientar LLMs na geração de descrições de hardware que são garantidamente corretas sintaticamente, livres de defeitos que quebram a síntese e verificadas funcionalmente por meio de provas verificadas por máquina, alcançando assim uma realizabilidade de backend quase perfeita e permitindo otimização segura e automatizada de PPA.

Autores originais: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Publicado 2026-05-11

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

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

Imagine que você está pedindo a um arquiteto muito talentoso, mas ligeiramente descuidado, que desenhe uma planta baixa para uma casa com base em uma descrição verbal.

No mundo tradicional do projeto de chips, você pediria ao arquiteto que escrevesse as instruções em Verilog (uma linguagem usada para descrever chips de computador). O arquiteto poderia escrever uma descrição bela, mas, como o Verilog é um pouco como um conjunto solto de regras, o arquiteto poderia acidentalmente dizer: "Conecte um tubo de 4 polegadas a um tubo de 8 polegadas" ou "Crie um corredor que se loopa de volta para si mesmo".

O computador verifica a gramática e diz: "Parece bom!" Mas quando a casa é realmente construída (o chip é fabricado), esses erros fazem os tubos estourarem ou o corredor prender pessoas. São falhas silenciosas e caras que só aparecem semanas depois.

CKTFORMALIZER é um novo framework que muda o jogo. Em vez de deixar o arquiteto escrever diretamente na linguagem solta do Verilog, ele força-os a escrever em uma linguagem matemática estrita chamada Lean.

Veja como funciona, usando uma analogia simples:

1. O Editor Estrito (O Compilador)

Pense no Lean como um editor superestrito que sabe exatamente como uma casa deve ser construída.

O Jeito Antigo: O arquiteto escreve "Conecte o tubo A ao tubo B". O editor não verifica os tamanhos. Mais tarde, a equipe de construção descobre que o tubo A é pequeno demais.
O Jeito CKTFORMALIZER: O arquiteto tenta escrever "Conecte o tubo A (tamanho 4) ao tubo B (tamanho 8)". O editor imediatamente fecha a porta e diz: "Erro! Você não pode conectar estes. Corrija agora."
O Resultado: O arquiteto (uma IA) recebe feedback instantâneo. Eles não podem avançar até que os tamanhos coincidam perfeitamente. Isso detecta "desajustes de largura" e "loops" antes que um único tijolo seja assentado.

2. A Rede de Segurança (Segurança de Tipos)

No sistema antigo, você poderia acidentalmente deixar uma porta aberta em um cômodo, e a casa seria construída com um cômodo rascunhoso e quebrado. No sistema Lean, as regras são tão estritas que é fisicamente impossível escrever uma planta baixa com um cômodo quebrado.

Se o arquiteto esquecer de descrever o que acontece quando um interruptor é acionado, o editor diz: "Você perdeu um caso! Você deve descrever todas as possibilidades."
Isso garante que o projeto seja "correto por construção". Se compilar (passar na verificação do editor), é garantido que seja estruturalmente sólido.

3. A Prova da Verdade (Verificação Formal)

Geralmente, para verificar se um projeto de casa funciona, você constrói um modelo pequeno e o testa. Às vezes o modelo funciona, mas a casa real não.
O CKTFORMALIZER usa provas matemáticas. A IA não apenas adivinha; ela escreve uma prova matemática que diz: "Este novo projeto, mais barato, faz exatamente a mesma coisa que o projeto original perfeito."

É como ter um matemático provando que seu novo projeto, mais barato, é 100% idêntico em função ao original, átomo por átomo, para cada cenário possível, não apenas para aqueles que você testou.

4. O Ciclo de Otimização (O Reformador Inteligente)

Uma vez que a IA tem um projeto que funciona, o sistema não para. Ele age como um reformador inteligente que olha para a planta baixa e diz: "Podemos tornar esta casa 35% menor e usar 30% menos energia."

A IA tenta rearranjar os cômodos (a lógica do circuito).
Ela constrói uma nova versão.
Ela executa imediatamente o "Editor Estrito" novamente para garantir que a nova versão ainda funcione perfeitamente.
Em seguida, ela executa uma simulação física para ver quanto espaço e energia ela economiza.
Se a nova versão for melhor e ainda for matematicamente provada como correta, ela a mantém. Se não, ela desfaz.

Os Resultados

O artigo testou isso em centenas de problemas de projeto (como construir contadores, unidades de memória e controladores de semáforos).

A Linha de Base (Jeito Antigo): Quando tentaram fabricar os chips, cerca de 20% dos projetos que pareciam corretos no papel falharam realmente quando tentaram fabricá-los.
CKTFORMALIZER (Jeito Novo): 100% dos projetos que passaram pelo editor estrito passaram com sucesso por todo o processo de fabricação (síntese, colocação e roteamento) sem falhar.
Eficiência: O sistema também conseguiu reduzir os projetos e economizar energia significativamente (até 35% menos área) enquanto provava que ainda eram perfeitos.

Em Resumo

O CKTFORMALIZER é como dar a um arquiteto de IA um livro de regras mágico que impede que eles cometam erros antes mesmo de começarem a desenhar. Em vez de construir uma casa e torcer para que ela não desabe, ele força o arquiteto a provar que a casa é sólida antes de encomendar o primeiro tijolo. Isso transforma o projeto de chips de um jogo de "adivinhar e verificar" em um processo de "provar e construir", resultando em chips menores, mais eficientes e garantidos para funcionar.

Resumo Técnico: CktFormalizer

Declaração do Problema

O projeto de hardware permanece uma disciplina propensa a erros, onde defeitos sutis, como incompatibilidades de largura de bits, loops combinatórios ou lógica de caso incompleta em Máquinas de Estado Finito (FSMs), podem passar por verificações de sintaxe, mas falhar silenciosamente durante a síntese ou manifestar-se como bugs de silício custosos posteriormente. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham demonstrado a capacidade de gerar Verilog a partir de especificações em linguagem natural, o código resultante frequentemente herda as armadilhas inerentes do Verilog e do VHDL: a falta de garantias estáticas como tipos dependentes, correspondência de padrões exaustiva e provas verificadas por máquina. Consequentemente, o hardware gerado por LLMs frequentemente requer extensa depuração manual e muitas vezes falha em alcançar a implementação física (Place-and-Route, DRC, LVS), mesmo quando funcionalmente correto na simulação.

Metodologia

O artigo apresenta o CktFormalizer, um framework que unifica a geração de código orientada por LLMs com verificação formal, visando uma Linguagem de Descrição de Hardware (HDL) com tipos dependentes incorporada no Lean 4. Em vez de gerar Verilog diretamente, o sistema redireciona o agente LLM para gerar código Lean, que serve como o alvo principal de compilação.

Arquitetura Central

O framework opera através de um pipeline em malha fechada envolvendo três papéis distintos para o Lean:

Verificador de Tipos (Verificador em Tempo de Compilação): O sistema de tipos dependentes do Lean codifica restrições de largura de bits, cobertura de casos e aciclicidade. Defeitos de hardware (por exemplo, incompatibilidades de largura ou loops combinatórios) são detectados como erros de tipo em tempo de compilação, em vez de falhas silenciosas no backend. Isso fornece ao agente LLM feedback imediato e acionável para reparar iterativamente o projeto.
Firewall de Corretude: Projetos que compilam com sucesso no Lean são estruturalmente garantidos como livres de classes específicas de defeitos (incompatibilidades de largura, loops combinatórios, latches não intencionais). Isso garante que os projetos compilados sobrevivam ao fluxo de síntese backend e Place-and-Route (P&R) sem a taxa de perda de 20% observada na geração de Verilog de base.
Assistente de Prova: O agente constrói provas de teoremas automatizadas para verificar a equivalência funcional entre a especificação em linguagem natural e a implementação gerada (ou otimizada). Essas provas cobrem sequências de entrada arbitrárias e larguras parametrizadas, indo além das limitações da verificação baseada em SMT limitada.

Fluxo de Trabalho

Geração e Iteração: Um agente LLM (instanciado com Claude) gera código HDL em Lean com base em uma especificação em linguagem natural. Ele entra em um loop iterativo "gerar-compilar-reparar", onde erros do compilador Lean orientam o agente a corrigir bugs semânticos antes que eles se propaguem.
Extração: Após a compilação bem-sucedida, um metaprograma (#synthesizeVerilog) extrai SystemVerilog sintetizável do grafo de combinadores de sinal do Lean.
Implementação Física: O SystemVerilog extraído é simulado, sintetizado (usando Yosys) e implementado fisicamente (usando OpenROAD com o PDK de 130nm da SkyWater) para gerar layouts GDSII e métricas de Potência-Desempenho-Área (PPA).
Loop de Otimização PPA: Uma etapa de otimização em malha fechada alimenta as métricas PPA de volta ao agente. O agente propõe variantes arquitetônicas (por exemplo, caminhos de dados paralelos vs. seriais) e deve fornecer provas de equivalência verificadas por máquina para garantir que a variante otimizada permaneça funcionalmente equivalente à especificação original.

Contribuições Principais

Primeiro Framework End-to-End: O CktFormalizer é o primeiro framework a combinar a geração de hardware orientada por LLMs com uma HDL incorporada no Lean, fornecendo um pipeline da linguagem natural ao silício sintetizável com otimização PPA em malha fechada.
Geração Guiada por Tipos: O artigo demonstra que visar uma HDL segura em tipos melhora substancialmente as taxas de sucesso dos LLMs em comparação com a geração direta de Verilog. Erros de tipo em tempo de compilação fornecem feedback estruturado que guia o agente em direção a projetos corretos, escalando para IP relevante para a indústria, como interfaces de barramento de handshake multicanal.
Integração de Verificação Formal: O framework preenche a lacuna entre código gerado por LLMs e hardware comprovadamente correto, permitindo que o agente produza provas de equivalência verificadas por máquina. Isso garante que otimizações arquitetônicas não comprometam a corretude funcional.

Resultados Experimentais

O framework foi avaliado em três benchmarks: VerilogEval (156 problemas), RTLLM (50 problemas) e ResBench (56 problemas).

Realizabilidade Backend: Uma descoberta crítica é que o CktFormalizer preserva a corretude funcional através do backend. Enquanto a base (geração direta de Verilog) perde aproximadamente 20% dos projetos funcionalmente corretos durante a síntese e roteamento, o CktFormalizer preserva 100% de seus projetos compilados através do fluxo completo de síntese, P&R, DRC e LVS.
Compilação e Simulação: No VerilogEval, o CktFormalizer alcançou uma taxa de compilação Lean de 92,3% e uma taxa de aprovação de simulação RTL de 72,4%, competitivas com as bases de geração direta de Verilog. Quando o feedback de síntese é incluído no loop do agente, a taxa de compilação sobe para 99,4%.
Otimização PPA: A etapa de otimização em malha fechada produziu melhorias significativas. Através de exploração de arquitetura validada, o framework alcançou até 35% de redução de área e 30% de redução de potência.
Fechamento de Temporização: Todos os projetos funcionalmente corretos que completaram o Place-and-Route alcançaram o fechamento de temporização (WNS $\ge$ 0 ns) sem intervenção manual.
Geração de Provas: Em um estudo piloto, a geração passo a passo de provas (refinamento iterativo com feedback de objetivo de prova) melhorou as taxas de conclusão de provas de 53% para 63%, demonstrando a viabilidade de assistentes de prova para verificação de hardware.

Significado e Alegações

O artigo alega que tipos dependentes e agentes LLM são complementares. Ao usar uma linguagem formal (Lean) tanto como alvo de geração quanto como substrato de verificação, o framework transforma o loop "gerar-e-testar" do LLM de uma busca estocástica sobre programas sintaticamente válidos em um processo de refinamento guiado por tipos.

Os autores enfatizam que o compilador atua como o verificador, deslocando a detecção de erros do final do pipeline EDA (onde correções são custosas) para o tempo de compilação. Essa abordagem permite que o sistema produza hardware que não apenas é funcionalmente correto, mas também estruturalmente robusto contra transformações backend, resolvendo efetivamente o problema de "falha silenciosa" comum em hardware gerado por LLMs. O trabalho sugere que linguagens formais podem servir como base para design de hardware automatizado e confiável, permitindo que LLMs naveguem nas complexas compensações da otimização de hardware enquanto mantêm garantias rigorosas de corretude.