QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

O artigo apresenta o QiMeng-CodeV-SVA, um framework de síntese de dados bidirecional que treina modelos especializados para gerar afirmações SystemVerilog (SVAs) a partir de requisitos em linguagem natural, superando a escassez de dados reais e alcançando desempenho superior ao de grandes modelos de linguagem gerais.

O essencial

Imagine que você é um arquiteto construindo um arranha-céu gigante (o Hardware). Antes de colocar o primeiro tijolo, você precisa escrever um manual de instruções muito detalhado, dizendo exatamente como o prédio deve se comportar em cada situação: "Se o elevador estiver cheio, ele não pode subir", "Se houver um terremoto, as portas devem travar", etc.

No mundo dos chips de computador, esse manual é escrito em uma linguagem chamada RTL (o código do chip) e as regras de segurança são chamadas de SVA (Aserções em SystemVerilog).

O problema é que escrever essas regras de segurança é como tentar adivinhar todos os cenários de um filme de ação antes de filmá-lo. É chato, difícil e exige especialistas caríssimos. Se você errar uma regra, o chip pode falhar catastróficamente depois de fabricado.

Recentemente, tentamos usar Inteligência Artificial (LLMs) para escrever essas regras automaticamente. Mas, até agora, essas IAs eram como "generalistas": elas sabiam um pouco de tudo (literatura, culinária, programação), mas não eram especialistas em hardware. Elas cometiam erros sutis e perigosos.

Aqui entra o QiMeng-CodeV-SVA, o novo método apresentado neste artigo. Vamos entender como eles fizeram isso usando uma analogia simples:

1. O Problema: Falta de "Livros de Receitas" de Qualidade

Para ensinar uma IA a escrever regras de segurança, você precisa de milhares de exemplos de "Regra de Segurança + Código do Chip" que sejam perfeitos.

• O Desafio: Não existem muitos desses exemplos prontos na internet. Os que existem são poucos, antigos ou escritos por humanos de forma inconsistente.
• A Solução Criativa: Em vez de esperar os livros, eles criaram os livros. Eles pegaram milhares de projetos de chips de código aberto (como se fossem plantas de casas prontas) e pediram para uma IA inteligente analisar essas plantas e inventar as regras de segurança para elas.

2. O Truque do Espelho (Tradução Bidirecional)

Aqui está a parte mais genial do método. Como saber se a regra que a IA inventou está realmente correta e não é apenas "encheção de linguiça"?

Eles usaram uma técnica chamada Tradução Bidirecional, que funciona como um espelho de verdade:

1. O Espelho da Esquerda (Código para Texto): A IA pega a regra técnica (SVA) e a traduz para uma linguagem humana simples (ex: "O elevador não sobe se estiver cheio").
2. O Espelho da Direita (Texto de volta para Código): A IA pega essa explicação simples e tenta reescrever a regra técnica original.
3. O Teste do Espelho: Se a regra que saiu do "Espelho da Direita" for idêntica (ou logicamente equivalente) à regra original que entrou no "Espelho da Esquerda", então a IA entendeu perfeitamente o significado.
   • Se elas forem diferentes: Significa que a IA "alucinou" ou perdeu algum detalhe importante no meio do caminho. A regra é descartada.

Isso é como pedir para um tradutor traduzir um poema do português para o inglês e depois de volta para o português. Se o poema final for o mesmo que o original, o tradutor é bom. Se mudar o sentido, o tradutor precisa ser trocado.

3. O Treinamento do "Especialista"

Com milhões de exemplos filtrados por esse "espelho de verdade", eles treinaram um modelo de IA específico (o CodeV-SVA).

• Eles não usaram apenas qualquer IA; eles pegaram modelos de código aberto (como o Qwen) e os "especializaram" apenas nessa tarefa de hardware.
• Eles também ensinaram a IA a "pensar antes de falar" (adicionando um rascunho de raciocínio), assim como um engenheiro faz cálculos no papel antes de desenhar o projeto final.

4. O Resultado: O Mestre da Segurança

Quando testaram esse novo especialista:

• Ele superou gigantes da tecnologia como o GPT-5 e o DeepSeek-R1 (que são IAs muito caras e poderosas, mas generalistas).
• Ele conseguiu gerar regras de segurança corretas em 75,8% dos casos (em testes humanos), enquanto as IAs gerais ficavam atrás.
• O melhor de tudo: É um modelo menor e mais barato de rodar do que os gigantes proprietários.

Resumo da Ópera

Os pesquisadores perceberam que, para ensinar uma IA a ser um especialista em hardware, não adianta apenas jogar mais dados na mesa. É preciso garantir a qualidade desses dados.

Eles criaram uma fábrica de dados onde:

1. Pegam projetos reais de chips.
2. Pedem para a IA inventar regras.
3. Usam o "Teste do Espelho" (tradução ida e volta) para garantir que a regra faz sentido.
4. Descartam qualquer coisa que não passe no teste.
5. Treinam um "super-engenheiro" de IA com esses dados limpos.

O resultado é uma ferramenta que ajuda a garantir que os chips do futuro (seus celulares, carros e computadores) não tenham falhas de segurança, tudo feito de forma mais rápida, barata e precisa do que nunca.

Resumo técnico

Resumo Técnico: QiMeng-CodeV-SVA

1. O Problema

A verificação formal baseada em afirmações (assertions) é crucial no fluxo de design de hardware digital. Os engenheiros precisam traduzir especificações em linguagem natural e código RTL (Register Transfer Level) para Sistemas de Afirmações em SystemVerilog (SVAs). No entanto, existem desafios significativos na automação dessa tarefa usando Grandes Modelos de Linguagem (LLMs):

• Escassez de Dados de Alta Qualidade: Existem poucos corpora públicos de SVAs escritos por humanos (limitados a livros didáticos e alguns repositórios de código aberto), enquanto há abundância de código RTL.
• Ineficácia de LLMs Genéricos: Modelos de propósito geral (como GPT-5 ou DeepSeek-R1) performam mal na tradução NL2SVA (Natural Language to SVA) devido à falta de conhecimento especializado e à complexidade da sintaxe de SVA.
• Dificuldade de Validação Semântica: Métodos atuais de seleção de dados (como "LLM-as-a-judge" ou verificação formal simples) falham em detectar erros sutis. Por exemplo, uma afirmação trivial (ex: assert property (1'b1)) passa na verificação formal, mas não corresponde à descrição em linguagem natural. Da mesma forma, LLMs podem não perceber erros de precedência de operadores que tornam uma afirmação logicamente vazia.

2. Metodologia

Os autores propõem o CodeV-SVA, um pipeline de síntese de dados e treinamento de modelos especializados. O framework consiste em quatro etapas principais:

A. Síntese de SVA a partir de Código RTL Real (RTL-Grounded)

• Em vez de depender de SVAs existentes, o framework utiliza grandes quantidades de código RTL de código aberto (do dataset CodeV) como "Dispositivos Sob Teste" (DUTs).
• Um LLM genérico (DeepSeek-V3.1) analisa o RTL e as especificações para gerar múltiplas propriedades em linguagem natural e seus correspondentes SVAs.
• Uma ferramenta de verificação formal (JasperGold) filtra os SVAs gerados, mantendo apenas aqueles que são logicamente válidos sob o RTL específico. Isso gera um conjunto de dados inicial de 159k instâncias.

B. Seleção Bidirecional de Dados (Bidirectional Data Selection)

• Para garantir que o SVA gerado corresponda semanticamente à propriedade em linguagem natural, o framework aplica uma verificação de equivalência bidirecional:
  1. O SVA original é traduzido de volta para linguagem natural (SVA2NL).
  2. Essa nova descrição em linguagem natural é traduzida novamente para SVA (NL2SVA).
  3. O novo SVA é comparado com o original usando verificação formal.
• Critério de Aceitação: Apenas os pares (NL, SVA) onde o SVA re-gerado é logicamente equivalente ao original são mantidos. Isso elimina dados onde a tradução perdeu informações ou introduziu erros sutis (como o exemplo de precedência de operadores mostrado no artigo).

C. Refinamento Adicional de Qualidade

• LLM-as-a-judge com Priors de Especialistas: Um LLM é instruído a filtrar erros específicos identificados por humanos (ex: inconsistência de sinais, mal-entendido do RTL).
• Filtragem de Dificuldade: Um modelo mais fraco (Qwen3-8B) tenta gerar SVAs para as mesmas entradas. Se ele conseguir gerar SVas equivalentes facilmente, o dado é considerado trivial e removido para focar em casos complexos.
• Aumento de Trajetórias de Raciocínio: Um modelo de raciocínio avançado (DeepSeek-R1) gera trajetórias de pensamento (Chain-of-Thought) para os pares de dados, enriquecendo o conjunto de treinamento.

D. Ajuste Fino Supervisionado (SFT)

• O conjunto de dados final refinado (83k instâncias) é usado para fazer o fine-tuning de modelos de código aberto (Qwen3-8B e Qwen3-14B), resultando nos modelos CodeV-SVA.

3. Principais Contribuições

• Framework de Síntese de Dados RTL-Grounded: Demonstra que é possível gerar um corpus massivo e diversificado de SVAs de alta qualidade usando código RTL real como base, superando a escassez de dados existentes.
• Método de Seleção Bidirecional: Propõe uma técnica robusta para validar a equivalência semântica entre NL e SVA, superando as limitações de validadores puramente formais ou baseados em LLMs.
• Modelos Especializados de Alto Desempenho: Criação do CodeV-SVA, que supera modelos genéricos massivos em tarefas específicas de hardware, com custos de implantação muito menores.

4. Resultados

Os modelos foram avaliados nos benchmarks FVEval-NL2SVA (Human e Machine), medindo a correção funcional (Func.@k).

• Desempenho Superior: O CodeV-SVA-14B alcançou 75.8% no benchmark NL2SVA-Human e 84.0% no NL2SVA-Machine (Func.@1).
• Comparação com SOTA: O modelo superou ou igualou modelos proprietários de ponta como GPT-5 e DeepSeek-R1, que são significativamente maiores e mais caros para implantar.
• Ganhos com Dados Sintéticos: O modelo CodeV-SVA-8B mostrou um ganho de ~40% em relação à sua base (Qwen3-8B), provando que a qualidade dos dados sintetizados é o fator chave.
• Estudo de Ablação: A etapa de seleção bidirecional foi identificada como a mais crítica, trazendo um ganho de 12.3% na precisão Func.@1 e reduzindo o tamanho dos dados necessários em 34% para manter a eficiência.
• Cenário End-to-End: Em um fluxo de verificação automatizado (modificando o framework AssertionForge), o CodeV-SVA-8B gerou até 3.5x mais SVAs verificáveis do que o DeepSeek-R1 em designs complexos (como o OPENMSP430).

5. Significância

Este trabalho é significativo porque resolve o "gargalo de dados" na verificação de hardware usando IA. Ao invés de depender de dados escassos e caros de engenharia humana, o método propõe um ciclo de auto-supervisão baseado em RTL real.

• Viabilidade Econômica: Permite que empresas de hardware utilizem modelos menores e mais baratos (8B/14B) com desempenho superior a modelos gigantes, facilitando a adoção de IA em fluxos de trabalho de EDA (Electronic Design Automation).
• Qualidade e Confiabilidade: A introdução da seleção bidirecional oferece uma nova metodologia para garantir a precisão semântica em tarefas de tradução técnica, que pode ser aplicada a outros domínios além de hardware.
• Open Source: Os autores planejam liberar o dataset, os modelos e o pipeline de treinamento, o que deve acelerar a pesquisa em verificação formal assistida por IA.