Oito Provas Formais Verdes Viraram Cinco Homologáveis Quando Auditei as Asserções em SystemVerilog
Eu vi um painel formal sintético relatar 8/8 PROVEN, e depois vi sua própria auditoria certificar apenas 5/8 como TRUSTWORTHY. Essa reversão é a premissa do Proof Firewall, nossa demonstração executável de governança para asserções em SystemVerilog (SVA) geradas por IA, e ela mudou o padrão que exijo que uma prova verde atenda antes de chegar a uma revisão de sign-off de tape-out.
Construí o painel com propriedades "criadas por LLM" baseadas em fixtures em um árbitro sintético, um pipeline de dois estágios e um cruzamento de CDC porque o caso desconfortável merece ser visível. Uma asserção pode parecer perfeitamente respeitável em um registro de propriedades. Um mecanismo formal pode retornar um resultado verde. No entanto, a implicação pode nunca ter precisado realizar nenhum trabalho, ou pode continuar passando depois que o comportamento relevante do projeto foi quebrado. Eu vinha tratando a palavra PROVEN como um destino. Construir esta demonstração me forçou a tratá-la como o início de uma revisão de evidências.
A demonstração do Proof Firewall não substitui um mecanismo formal, não ingere RTL real nem chama um LLM em tempo real em seu fluxo padrão. Ela é deliberadamente menor e mais inspecionável: um model checker de estados explícitos em Python puro avalia uma IR sintética de sistema de transição; em seguida, um gate de governança verifica a alcançabilidade do antecedente, a eliminação de mutações e o cone de influência (COI). A saída é um motivo para registrar um certificado de demonstração assinado ou um motivo para reter o resultado para revisão humana.
Comecei com o tipo errado de verde
Lembro-me de que a primeira versão do painel transmitia segurança precisamente por ser tão limpa. Oito propriedades, oito selos verdes e uma visão de fluxo básico que fazia o trabalho parecer concluído. Meu instinto inicial foi fazer a demonstração explicar melhor esse resultado limpo. Achei que a tarefa de engenharia era de apresentação: exibir as provas, mostrar as asserções, tornar o dashboard mais fácil de confiar. O resultado verde era real, mas estava respondendo a uma pergunta menor do que aquela que um revisor precisa fazer.
Depois, submeti as mesmas oito propriedades às verificações que uma discussão de aprovação realmente exige. O antecedente alguma vez se tornou verdadeiro? A asserção contestaria se uma parte relevante do projeto fosse alterada? Ela restringe um COI significativo? Essas perguntas são menos lisonjeiras do que um selo verde porque questionam o que a prova conquistou, e não apenas o que o solver retornou.
Tive que abandonar o enquadramento inicial da implementação. Uma tela que exibia 8/8 PROVEN era uma visão precisa da linha de base de fluxo direto, mas estava incompleta como narrativa de sign-off. Após a auditoria do firewall, o mesmo painel sintético fixo tem cinco resultados TRUSTWORTHY, um resultado VACUOUS e dois resultados WEAK. Os três restantes não são rotulados novamente como sucesso. Eles são retidos juntamente com as evidências que explicam o motivo. Um rótulo de prova e uma decisão de homologação são artefatos diferentes.
Escolhi a palavra "governança" com muito cuidado aqui. As verificações determinísticas da demonstração tornam a decisão de homologação auditável. Um autor opcional de SVA pode propor uma asserção, mas o model checker e o gate de políticas determinam o veredito. Agentes aconselham, o código decide. Eu estava tentando tornar o gate legível o suficiente para que o resultado negativo fosse útil, em vez de apenas embaraçoso. Um resultado retido precisa de um motivo que um engenheiro de verificação possa inspecionar, reproduzir e contestar.
ARB3 tornou o problema impossível de ignorar
Encontrei a falha mais evidente em ARB3, a propriedade de árbitro sintético assert (g0 && g1) |-> (turn == 0). No fluxo básico, ela é verde. Quando abri sua forma de onda e as evidências de alcançabilidade, o antecedente g0 && g1 era inalcançável naquele árbitro sintético. A implicação havia sido provada apenas no sentido estrito de que nunca foi forçada a responder pelo estado que descrevia. O antecedente nunca dispara.
Essa distinção é fácil de enunciar e difícil de manter em mente quando um dashboard de verificação está repleto de verde. Inicialmente, li a implicação como uma afirmação sobre o comportamento de arbitragem. O resultado de alcançabilidade mudou o que eu estava observando. Era uma afirmação cuja condição de disparo nunca ocorria. Chamar isso de VACUOUS é mais útil do que preservar um rótulo verde, porque direciona o revisor para a premissa ou estímulo que tornou a prova vazia.
Continuei voltando a este painel enquanto trabalhava nos rótulos de política. VACUOUS pode parecer um resultado severo até que se considere a alternativa. Se um registro de sign-off mantiver uma prova sem registrar que seu antecedente nunca dispara, a revisão terá recebido uma conclusão sem a condição que lhe dá sentido. O melhor registro é aquele que torna a limitação explícita e deixa para o humano algo concreto a ser interrogado. Esse registro de alcançabilidade deve ficar ao lado do veredito.
Eu também precisei resistir a tratar a vacuidade como um aviso cosmético. Se a propriedade tem o objetivo de restringir uma condição de arbitragem, um comportamento de disparo inalcançável é uma evidência central sobre se a propriedade exerceu ou não o comportamento pretendido. O dashboard não deve exigir que o revisor deduza isso a partir de um resultado verde. Ele deve preservar a constatação de alcançabilidade, retirar o resultado do fluxo de certificação e deixar evidente a próxima ação de revisão.
O contexto do setor tornou o cenário ainda mais crítico para mim. O estudo de 2024 do Wilson Research Group / Siemens EDA citado na especificação da demonstração relata 14% de sucesso no primeiro silício. Essa não é uma medição da Veriprajna, e este painel sintético não pretende explicar esse número. Isso realmente me torna menos disposto a tratar um estado visualmente agradável do dashboard como evidência por si só.
A propriedade do pipeline sobreviveu à quebra que eu esperava que ela capturasse
Encontrei a segunda falha ao testar PIPE3, uma propriedade de pipeline sintético de dois estágios: assert v2 |-> (s2 == s2). Eu queria um exemplo conciso de uma asserção que soasse plausível o suficiente para passar despercebida em uma revisão superficial. O consequente é uma tautologia. Ele diz que s2 é igual a si mesmo. O consequente não restringe nada.
O ponto importante na demonstração não é apenas identificar a tautologia no texto. O gate de governança injeta mutações pontuais relevantes no projeto e verifica se a propriedade as elimina. Para o caso apresentado de pipeline fraco, PIPE3 registra um resultado de 0/6 mutações eliminadas. A propriedade sobrevive às variantes quebradas relevantes. É por isso que a política atribui WEAK em vez de permitir que o resultado bruto PROVEN permaneça como evidência para homologação. O resultado da mutação testa uma sensibilidade útil.
Aprendi algo desconfortável ao tentar fazer este exemplo parecer menos óbvio. Um ser humano pode ler s2 == s2 e descartá-lo rapidamente. Muitas fragilidades não se anunciarão de maneira tão clara. Por isso, não quis que a demonstração dependesse do operador identificar uma cadeia suspeita. O artefato útil é o procedimento: alcançabilidade, um teste relevante de eliminação por mutação, COI e uma decisão de política que registra sua justificativa.
Passei a ver a verificação de mutação como uma forma disciplinada de recusar uma interpretação excessivamente conveniente de uma prova. O objetivo não é fabricar uma falha dramática. É perguntar se a propriedade notaria uma alteração local relevante no comportamento que deveria restringir. Quando não nota, o resultado informa ao revisor algo acionável: esta asserção precisa ser reforçada ou seguir um fluxo de revisão diferente antes de poder embasar o registro de sign-off.
É também por isso que o benchmark da demonstração exige uma descrição precisa. Sua execução local python -m backend.bench pontua 18/18 em relação a um conjunto fixo de asserções sintéticas rotuladas e identifica 6 provas que a linha de base sem verificações da própria demonstração teria aprovado cegamente. Esses números são uma verificação de reprodutibilidade nas fixtures rotuladas desta demonstração. Não são uma taxa de produção, uma alegação sobre asserções geradas por IA em geral ou uma comparação com ferramentas formais comerciais.
Deixei de tentar fazer o gate parecer permissivo
Tive uma escolha de design após os primeiros resultados de auditoria: abrandar os vereditos retidos para que o painel parecesse mais otimista, ou deixar o painel recusar a certificação daquilo que não podia defender. Optei pelo segundo caminho porque uma revisão real de sign-off precisa da capacidade de distinguir uma prova completa de uma limitada, um antecedente inalcançável de uma propriedade significativa e uma verificação fraca de uma que reage a comportamentos defeituosos relevantes. A retenção é um resultado de revisão, não um beco sem saída.
Essa escolha se reflete no vocabulário de políticas. TRUSTWORTHY obtém o certificado assinado de demonstração. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD e VIOLATED preservam diferentes motivos para reter esse certificado ou encaminhar o resultado para escalonamento. Na fixture de CDC, por exemplo, a propriedade mais forte assert (req && !ack) |-> ##1 req é VIOLATED e produz uma forma de onda sintética concreta de contraexemplo. Ela ilustra uma classe de falha de transação perdida ou de CDC. Não diz nada sobre um chip de cliente.
Não vejo isso como uma proposta para substituir o mecanismo existente de uma equipe de verificação. A direção para produção independe de mecanismo: colocar um gate em torno de um fluxo formal existente e tornar seus critérios de aceitação inspecionáveis. Adaptadores para motores reais e ingestão de RTL foram postergados nesta demonstração. A fronteira demonstrada é intencionalmente estreita. Essa fronteira é importante porque mantém a alegação proporcional ao que está de fato em execução.
Agora eu quero o comprovante ao lado do veredito
Fico pensando no artefato de que uma reunião de sign-off precisa quando o autor da asserção conta com auxílio de IA. Não se trata de uma pontuação de confiança fornecida pelo autor. Trata-se de um registro que indica quais verificações foram executadas, qual foi o resultado de alcançabilidade, quais mutações foram eliminadas, o que o COI continha e por que a política concedeu ou reteve a certificação. A revisão precisa de evidências que possam ser reabertas.
É exatamente isso que a demonstração exporta em signoff_certificate.json: vereditos por propriedade, alcançabilidade, resultados de mutação, COI, registros de contraexemplos onde aplicável e um campo SHA-256. Desenvolvi o certificado como um registro de demonstração porque um revisor deve ser capaz de reconstruir a decisão sem aceitar um selo verde por mera confiança. Um certificado deve preservar o caminho até seu veredito.
E se você prefere ver a me ler descrevendo, aqui está o sistema completo rodando de ponta a ponta.
Tornei a demonstração executável para que a reversão de 8/8 para 5/8 possa ser inspecionada em vez de repetida como um slogan. O resultado que tiro disso é modesto, mas duradouro: uma prova que vale a pena homologar traz evidências do que ela restringiu, ao que ela sobreviveu e por que alguém pode confiar nela. O verde continua sendo útil. Ele só precisa de um registro que permita ao próximo revisor decidir se ele merece ir além.
