Resumo Técnico: SpecAlign – Um Framework de Alinhamento Semântico para Geração de Asserções em SystemVerilog

1. Declaração do Problema

A crescente complexidade dos projetos de hardware modernos impulsionou a adoção de Modelos de Linguagem de Grande Porte (LLMs) para a geração de Asserções em SystemVerilog (SVA) a fim de apoiar a Verificação Baseada em Asserções (ABV). No entanto, as abordagens existentes de LLM focam principalmente na validade sintática e nos resultados da Verificação Formal (FV) (por exemplo, se uma asserção é provada ou gera um contraexemplo em um determinado RTL). Essas métricas falham em abordar o alinhamento semântico: se a asserção gerada reflete com precisão a intenção comportamental descrita na especificação em linguagem natural.

LLMs podem produzir asserções que são sintaticamente corretas e formalmente prováveis em uma implementação específica de RTL, mas são semanticamente ineficazes ou alucinadas. Por exemplo, uma asserção pode amostrar um clock na mesma borda que dispara a propriedade, tornando-a vazia apesar de passar na FV. Na ausência de um modelo RTL "dourado" para comparação, a inspeção manual de tais asserções é demorada e reduz a confiança. Além disso, os motores de FV enfrentam problemas de escalabilidade (explosão do espaço de estados) ao avaliar grandes conjuntos de asserções geradas para projetos complexos. Há uma necessidade crítica de um framework que avalie a consistência semântica contra a própria especificação, independentemente dos detalhes de implementação do RTL.

2. Metodologia: O Framework SpecAlign

O SpecAlign é um framework centrado na especificação projetado para avaliar e refinar iterativamente SVAs gerados por LLMs sem depender de RTL dourado. Ele opera através de dois loops iterativos principais: um Loop de Alinhamento de Propriedades e um Loop de Alinhamento de SVA. Ambos os loops utilizam três etapas centrais: Verificação de Alinhamento, Análise de Inconsistência e Extração de Evidências.

A. Visão Geral Arquitetural

O framework normaliza a comparação entre diferentes representações da intenção de projeto. Embora a entrada consista em propriedades em linguagem natural ($P$) e SVAs gerados ($A$), o framework converte cada SVA em um Resumo em Linguagem Natural ($N$) por meio de um processo de extração específico. Essa normalização permite que tanto as propriedades quanto as asserções sejam avaliadas no mesmo nível semântico contra a especificação de projeto ($S$).

B. Componentes Principais

1. Verificação de Alinhamento:

   • Classificação: O framework classifica descrições em linguagem natural ($X_i$) em três categorias com base em sua relação com a especificação:
     • Implica (Entails): Todos os elementos são suportados pela especificação.
     • Contradiz (Contradicts): Pelo menos um elemento contradiz a especificação.
     • Desconhecido (Unknown): Os elementos não são nem suportados nem contraditos (muitas vezes devido a suposições específicas de implementação não presentes na especificação).
   • Votação de Autoconsistência: Para melhorar a confiabilidade, o sistema emprega uma estratégia de prompt de Cadeia de Pensamento (CoT). Ele gera $k$ caminhos de raciocínio para uma entrada dada e agrega os sub-vereditos usando votação majoritária. Em caso de empate, aplica-se uma prioridade conservadora: Contradiz > Desconhecido > Implica.
   • Seleção de Referência: O Loop de Propriedades usa a especificação de projeto ($S$) como referência. O Loop de SVA usa um "Banco de Propriedades Alinhadas" (se disponível) para reduzir o ruído de documentos de especificação dispersos; caso contrário, recorre a $S$.

2. Análise de Inconsistência e Refinamento:

   • Quando um veredito é Contradiz, o sistema realiza uma Análise de Inconsistência. Ele identifica os elementos conflitantes específicos na descrição, referencia o comportamento correto na especificação e gera feedback estruturado e acionável ($F_i$).
   • Esse feedback guia o LLM a regenerar a propriedade ou asserção ($P'_i$ ou $A'_i$), definindo explicitamente as condições de disparo e evitando a introdução de novos sinais ou comportamentos não presentes na especificação.
   • A saída refinada é reavaliada no loop de alinhamento até que um número fixo de iterações seja atingido ou a saída esteja alinhada.

3. Extração de Evidências:

   • Para casos de Implica, o sistema extrai evidências de suporte (citações e localizações) da especificação para facilitar a revisão humana e fortalecer a confiança.
   • Para casos de Desconhecido, o sistema categoriza quais elementos são ambíguos ou indefinidos, distinguindo contradições reais de comportamentos subespecificados.

4. Métrica Quantitativa:

   • O framework define uma Pontuação de Alinhamento ($a_t$) calculada como a razão entre asserções que implicam ($E$) e o número total de asserções ($n$) em uma dada iteração ($a_t = E/n$). O objetivo do processo de refinamento é maximizar essa pontuação.

C. Extração de Resumo em Linguagem Natural

Uma etapa crítica de pré-processamento envolve a conversão de SVAs formais em resumos estruturados em linguagem natural. O LLM é instruído a identificar componentes específicos de SVA (Disparo, Antecedente, Operador de Implicação, Consequente e Desabilitar Se) e mapeá-los para frases equivalentes em linguagem natural. Isso garante que a intenção semântica do código formal seja preservada para comparação.

3. Contribuições Principais

O artigo descreve as seguintes contribuições:

• Framework de Avaliação Semântica: Uma abordagem inovadora para avaliar SVAs gerados por LLMs contra especificações em linguagem natural sem depender da verificação formal aplicada a RTL dourado.
• Pipeline de Refinamento Iterativo: Um framework estruturado composto por Verificação de Alinhamento, Análise de Inconsistência e Extração de Resumo de SVA, projetado para integração em fluxos de trabalho de geração baseados em LLM existentes.
• Métrica Quantitativa de Alinhamento: Uma métrica de pontuação de alinhamento baseada em classificação de implicação semântica para medir a consistência da especificação, oferecendo uma alternativa escalável à avaliação tradicional de correção via FV.
• Mecanismo de Análise de Inconsistência: Um método para gerar feedback específico e acionável para propriedades e asserções contraditórias, apoiando tanto a revisão manual quanto o refinamento automatizado.
• Validação Empírica: Resultados experimentais demonstrando a redução de asserções contraditórias em projetos APB e UART por meio de refinamento semântico.

4. Resultados Experimentais

Os autores avaliaram o SpecAlign em dois projetos de hardware: APB (Interface APB para I2C) e UART (Interface UART para Barramento). O framework foi comparado com o AssertionForge, um método de linha de base que utiliza um grafo de conhecimento e incorpora RTL na geração.

• Resultados APB:
  • Linha de Base (AssertionForge): Gerou 442 SVAs com uma pontuação de alinhamento de 0,02. Apenas 8 foram implicados, enquanto 148 foram contraditórios.
  • SpecAlign: Mantive 442 SVAs, mas aumentou a pontuação de alinhamento para 0,15. Crucialmente, o número de asserções contraditórias caiu para 0, com 66 asserções implicadas. Os 376 restantes foram classificados como Desconhecidos.
• Resultados UART:
  • Linha de Base: Gerou 325 SVAs com uma pontuação de alinhamento de 0,06 (21 implicados, 142 contraditórios).
  • SpecAlign: Gerou 319 SVAs com uma pontuação de alinhamento de 0,28. As asserções contraditórias foram reduzidas para 6, enquanto as asserções implicadas aumentaram para 92.

Análise dos Resultados:
Os experimentos revelaram que os métodos de linha de base frequentemente geram asserções que são ou contraditórias à especificação ou dependem fortemente de detalhes específicos de implementação (RTL) não encontrados na especificação em linguagem natural. O SpecAlign filtra efetivamente essas contradições. O aumento nas classificações "Desconhecido" no SpecAlign (por exemplo, 376 para APB) é interpretado não como uma falha, mas como uma estratégia de classificação mais conservadora e precisa que separa suposições específicas de implementação de comportamentos suportados pela especificação. Essa distinção previne o rótulo de falso positivo de comportamentos não suportados como "implicados".

5. Significado e Alegações

O artigo afirma que o SpecAlign fornece um complemento escalável à verificação formal tradicional. Ao separar a correção semântica dos resultados de prova do RTL, ele aborda a limitação de que a verificação formal sozinha não pode determinar se uma asserção captura o comportamento pretendido descrito na especificação.

Os autores enfatizam que, embora a verificação formal seja necessária para provar que as asserções se mantêm no RTL, ela é insuficiente para avaliar a qualidade da intenção da asserção. O SpecAlign melhora a confiança em asserções geradas por LLMs ao:

1. Detectar inconsistências semânticas que ferramentas formais podem perder (por exemplo, verdades vazias).
2. Reduzir esforços de depuração ao identificar contradições antes da simulação RTL ou prova formal.
3. Fornecer um mecanismo para refinar asserções iterativamente sem exigir um modelo dourado.

O artigo conclui com modéstia, observando que, embora o framework melhore o alinhamento, trabalhos futuros são necessários para refinar as metodologias de classificação, capturar melhor erros sintáticos e estender a abordagem para outras tarefas de automação de projeto de hardware, como geração e depuração de RTL.