Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

No mundo invisível dos microchips, onde bilhões de transistores ligam e desligam para alimentar desde smartphones até espaçonaves, um único erro oculto pode fazer com que um sistema falhe catastroficamente. Engenheiros projetam esses chips usando uma linguagem chamada Nível de Transferência de Registrador, ou RTL, que descreve como os dados se movem entre elementos de armazenamento ao longo do tempo. Para garantir que esses projetos funcionem corretamente antes de serem construídos, especialistas em verificação escrevem "asserções". Pense em uma asserção como uma regra estrita escrita no próprio projeto, uma afirmação que diz: "Se isso acontecer, então aquilo deve seguir". Se o chip violar essa regra, o sistema levanta um alarme, revelando um bug que, de outra forma, poderia passar despercebido. Por décadas, escrever essas regras tem sido uma tarefa lenta, manual e propensa a erros, exigindo que engenheiros adivinhassem quais comportamentos poderiam dar errado e escrevessem verificações específicas para eles. Embora os computadores tenham ajudado ao minerar simulações de projetos existentes para encontrar padrões, esses métodos automatizados frequentemente perdem os cenários mais perigosos simplesmente porque os testes aleatórios nos quais dependem nunca tropeçam neles.

Uma equipe de pesquisadores da Universidade de Ciência e Tecnologia de Hong Kong (Guangzhou) desenvolveu uma nova abordagem para resolver este problema, chamando seu sistema de NeuroAssertion. Em vez de depender do acaso para encontrar bugs, seu método busca ativamente os comportamentos mais difíceis de alcançar em um projeto de chip e, em seguida, utiliza uma combinação de inteligência artificial e lógica formal para escrever as regras de segurança necessárias. O processo começa transformando o projeto para torná-lo mais fácil de visualizar quais partes estão sendo testadas. Os pesquisadores inserem marcadores especiais no código que rastreiam se condições específicas e de difícil ativação já ocorreram. Eles então utilizam um poderoso motor matemático, conhecido como verificador de modelo (model checker), para forçar o projeto a executar essas condições raras. Isso gera um conjunto de casos de teste altamente específicos que expõem comportamentos que simulações aleatórias provavelmente perderiam para sempre. Esses novos traços diversos fornecem uma base muito mais rica para a próxima etapa.

Assim que o sistema possui esses comportamentos difíceis de encontrar, ele passa para a fase de geração. Ele utiliza uma técnica chamada síntese guiada por sintaxe para criar regras de segurança iniciais baseadas nos dados observados. No entanto, os pesquisadores reconheceram que essa primeira passagem raramente é perfeita. Para corrigir isso, introduziram um loop de refinamento que atua como um editor rigoroso. O sistema mede o quão bem o conjunto atual de regras consegue detectar mudanças no projeto ao injetar erros pequenos e deliberados, conhecidos como mutantes, no código. Se as regras falharem em capturar um mutante, o sistema sabe exatamente qual comportamento permanece não verificado. Ele então recorre a um grande modelo de linguagem para propor uma nova regra especificamente desenhada para cobrir essa lacuna. Se a regra proposta for logicamente falha, um segundo modelo de linguagem não a descarta; em vez disso, ele analisa o erro e constrói um conjunto especializado de instruções, ou gramática, para guiar um resolvedor simbólico na reparação da regra. Isso cria um ciclo onde o sistema propõe, verifica e corrige asserções até que elas sejam tanto numerosas quanto robustas.

Os resultados desta abordagem foram testados em sete designs de chips diferentes, variando de pequenos circuitos de arbitragem a núcleos de processadores complexos. O novo framework superou consistentemente o método de ponta anterior, conhecido como SMART, que depende de uma única passagem de mineração sem este refinamento ativo. Nestes experimentos, o NeuroAssertion gerou aproximadamente o dobro de asserções do que o método antigo. Mais importante ainda, a qualidade dessas regras foi significativamente maior. Quando medido pela sua capacidade de detectar erros injetados, o novo sistema alcançou cerca de duas vezes mais cobertura do que a abordagem tradicional. Em alguns benchmarks específicos, a melhoria foi ainda mais dramática; por exemplo, em um componente de processador, a cobertura de mutação saltou de aproximadamente seis por cento para mais de trinta e dois por cento. Os pesquisadores também compararam seu sistema contra uma abordagem direta onde um grande modelo de linguagem foi solicitado a escrever regras sem qualquer um dos passos de verificação formal ou refinamento. Esse método direto produziu muito menos regras e falhou em capturar a maioria dos erros potenciais, demonstrando que a geração pura de linguagem é insuficiente para esta tarefa de alto risco.

Ao tratar a geração de asserções como um loop contínuo de exploração e refinamento, em vez de um evento de uma única vez, os pesquisadores mostraram que é possível automatizar a criação de regras de segurança de alta qualidade para hardware complexo. O sistema não apenas adivinha; ele busca ativamente os pontos cegos em um projeto e utiliza uma parceria entre redes neurais e lógica formal para preenchê-los. Este trabalho sugere que o futuro da verificação de hardware reside na combinação do reconhecimento de padrões da inteligência artificial com a certeza rigorosa da prova matemática, garantindo que os chips que alimentam nosso mundo sejam tão confiáveis quanto os engenheiros que os projetam.