Os grandes modelos de linguagem estão próximos de executar uma das tarefas mais incômodas na verificação de projetos de chips: converter especificações escritas em linguagem natural em um conjunto de propriedades formais que possa ser usado para avaliar a correção de uma implementação RTL. Entrevistas conduzidas por Brian Bailey na Semiconductor Engineering mostram que as ferramentas atuais conseguem produzir um rascunho inicial útil, mas ainda estão longe de criar um conjunto completo que possa ser aprovado sem uma revisão de engenharia intensiva.
A importância desse desenvolvimento está no fato de que a escrita de propriedades representa há anos um gargalo na verificação formal. As propriedades SystemVerilog, conhecidas como assertions quando inseridas no ambiente de verificação, são usadas para descrever as relações lógicas e temporais entre os sinais, como o comportamento de reset, handshakes, condições one-hot e verificações básicas de segurança. Quando essas propriedades são completas e precisas, podem ser usadas para comparar o comportamento de uma implementação RTL com a especificação, sem depender da forma como o projeto foi construído.
O que as ferramentas conseguem fazer hoje?
Uma ferramenta baseada em um grande modelo de linguagem pode ler um documento de especificação, um padrão de protocolo ou até comentários dentro do RTL e, em seguida, propor um rascunho de propriedades SVA. Ashish Darbari, CEO da Axiomise, afirma que esse uso é mais viável quando as especificações se baseiam em padrões estáveis que não mudam muito. Nesse caso, a ferramenta reduz a parte repetitiva da escrita do código inicial, em vez de assumir todo o processo de verificação.
Algumas abordagens tentam melhorar a precisão dos modelos por meio da criação de um knowledge graph, ou seja, um grafo de conhecimento que armazena entidades e as relações entre elas. Os nós podem incluir um sinal, um módulo, um requisito ou uma porta, enquanto as arestas descrevem relações como “dirige”, “reinicia” e “responde a”. Em vez de recuperar trechos de texto que parecem relacionados à solicitação, o sistema pode consultar fatos e vínculos específicos, reduzindo a probabilidade de inventar o nome de um sinal ou interpretar incorretamente uma relação entre componentes do projeto. A fonte menciona, nesse contexto, uma pesquisa intitulada RAG-SVA in the Landscape of LLM-Based Assertion Generation, de Cohen e Chibani.
O problema começa antes da inteligência artificial
A ferramenta não consegue extrair aquilo que não foi escrito ou decidido originalmente. Ravindra Aneja, diretor de engenharia de aplicações da Synopsys, afirma que a especificação ideal não esteve disponível nas últimas três décadas; muitas vezes, o desenvolvimento começa antes que a documentação esteja completa, e alguns projetos podem não ter uma especificação completa, especialmente em projetos derivados ou quando os requisitos mudam durante o trabalho.
Esse problema não diz respeito apenas à redação, mas também ao gerenciamento de mudanças. A equipe de marketing pode adicionar um novo recurso ou modificar um requisito existente, e as equipes de projeto e verificação precisam determinar o impacto dessa alteração. Abhi Kolpekwa, vice-presidente sênior e gerente-geral da Siemens EDA, considera que converter a especificação em propriedades exige “inteligência contextual” capaz de acompanhar o histórico e o contexto das mudanças, e não um agente que gere um novo texto a cada vez.
O risco da falsa confiança
Uma das maiores limitações da abordagem atual é que a propriedade pode estar sintaticamente correta, ser traduzida e ter sua prova concluída pelas ferramentas de verificação, mas ainda assim não testar o comportamento realmente pretendido. Darbari alerta que uma propriedade fraca ou vacuous pode ser aprovada facilmente porque permite muitos comportamentos, porque usa o sinal errado ou porque contém uma condição antecedente ausente ou excessivamente restritiva. Por isso, uma “prova verde” não significa que o projeto esteja livre de erros: a evidência não é mais forte do que a propriedade que foi provada.
A fonte acrescenta que os modelos tendem a ter um desempenho melhor em cobertura estrutural e sintática do que na compreensão da intenção arquitetural e do motivo da existência da regra. Assim, uma leitura imprecisa da especificação pelo modelo pode se transformar em um trecho que parece formal e rigoroso, mas esconde uma lacuna nos requisitos. Se essa lacuna passar para trabalhos como FMEDA, arquivos de segurança ou evidências de certificação relacionadas à ISO 26262 e à ISO 21434, seu impacto poderá se estender muito além do projeto de verificação original.
A questão da separação entre projeto e verificação também ganha destaque. Kaye Mao, líder de design de produtos da Normal Computing, aponta a necessidade de restringir os materiais do projeto aos quais os agentes podem ter acesso, pois permitir que o agente use o próprio projeto para gerar casos de teste pode comprometer a independência do processo de verificação.
O que muda na prática?
A inteligência artificial pode reduzir o tempo de preparação dos primeiros rascunhos de dias para minutos, segundo Darbari, mas pode multiplicar o trabalho posterior. Cada propriedade gerada precisa ser verificada em relação à especificação, ter sua cobertura analisada, ser testada quanto à vacuity e passar por uma revisão de sua relação com os sinais do projeto; as falhas também podem exigir análise das formas de onda. Se o número de propriedades aumentar dez vezes e o nível de escrutínio exigido para cada uma permanecer o mesmo, o esforço de revisão poderá superar o ganho obtido com a geração rápida.
Na perspectiva da certi.news, a verdadeira mudança não é substituir o engenheiro de verificação, mas deslocar o centro de gravidade da escrita das propriedades para sua avaliação e rastreabilidade de origem. Darbari recomenda tratar as propriedades geradas como rascunhos, e não como resultados aprovados, e criar um portão de revisão antes de incorporá-las à regression suite. Também é necessário registrar a origem de cada propriedade — o parágrafo da especificação, o requisito ou o elemento RTL que a produziu — para que o engenheiro possa verificar a conformidade.
Essa abordagem pode reduzir a barreira de entrada para engenheiros de verificação que desejam usar formal verification, afirma Yaron Ilani, engenheiro de soluções de verificação da Normal Computing. No entanto, isso não resolve a questão do retorno sobre o investimento. Kaye Mao considera que o tempo gasto na verificação das saídas do agente deve ser contabilizado no custo, enquanto Arvind Srinivasan, chefe de engenheiros de soluções da Normal Computing, observa que a expansão não depende apenas da computação, mas também da completude dos dados e do custo da revisão humana.
A conclusão é que os grandes modelos de linguagem já são capazes de acelerar a parte automática e repetitiva da formulação de propriedades, mas ainda não resolveram os problemas de completude da especificação e de compreensão da intenção do projeto. O valor dessas ferramentas continuará ligado à existência de um engenheiro que compreenda o projeto e a mecanismos independentes para medir a cobertura e detectar propriedades vazias ou inadequadas, e não ao número de propriedades que o modelo consegue produzir.