TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

Resumo Técnico: TensorEQC – Verificação de Equivalência Sensível à Estrutura

Definição do Problema
A verificação de equivalência (EC) é altamente sensível à representação de um circuito. Diferentes estruturas de circuitos — como redes ricas em XOR, cadeias de carry, multiplicadores de corpos finitos e multiplicadores inteiros — exibem propriedades estruturais distintas que favorecem diferentes abordagens de verificação. Nenhum método único (por exemplo, álgebra booleana, diagramas de decisão ou redes de tensores) domina universalmente todos os tipos de circuitos. Além disso, verificar circuitos sequenciais requer distinguir entre a dependência do estado inicial observável e a incerteza que se resolve dentro de um limite de observação específico, particularmente em relação aos estados de reset.

Metodologia
O artigo apresenta o TensorEQC, um fluxo de trabalho de pesquisa executável projetado como um portfólio multialgorítmico, em vez de um único solver monolítico. Sua filosofia central é que um motor deve apenas descarregar uma obrigação de verificação se puder fazê-lo de acordo com sua própria semântica exata; caso contrário, a obrigação é passada para outro motor.

O fluxo de trabalho consiste em três componentes primários:

1. Portfólio Combinacional: Um pipeline sequencial de motores de verificação que processa saídas até que sejam descarregadas ou um limite de recursos seja atingido. O pipeline inclui:
   • Hashing Estrutural: Estabelece a identidade de DAGs de expressão sob primitivas suportadas (AND, OR, XOR, etc.) com normalização comutativa.
   • Simulação: Utiliza simulação empacotada com padrões aleatórios, todos-zero e todos-um para encontrar testemunhas negativas (contraexemplos).
   • Formas Normais Algébricas (ANF): Representa funções booleanas como polinômios multilineares sobre GF(2). Utiliza um lemma específico para gerar testemunhas negativas exatas a partir de polinômios não nulos.
   • Eliminação de Tensores Relacionais: Representa portas como tensores indicadores booleanos. Realiza a eliminação de variáveis via disjunção sobre o semiring booleano (para preservar a existência de atribuições satisfatórias) em vez de soma GF(2) (que computa paridade).
   • ROBDD & Fallback Exaustivo: Utiliza BDDs Ordenados com limites de nós (node caps) e enumeração exaustiva de suporte pequeno como fallbacks finais.
2. Análise de Tensor Train (TT): Um módulo complementar que constrói representações TT exatas a partir de tabelas de verdade para medir o rank algébrico e testar funções zero. Ele distingue entre ranks sobre GF(2) e números reais, observando que os ranks de GF(2) podem ser significativamente menores.
3. Análise de Reset: Um módulo síncrono que utiliza autocomposição de estado explícito para verificar a dependência do estado inicial. Distingue entre casos onde a dependência de reset é observável imediatamente e casos onde ela desaparece após um número específico de ciclos de "limpeza" (flushing).

Principais Contribuições

• Integração de Motores Exatos: O trabalho demonstra uma integração prática de hashing estrutural, álgebra GF(2), redes de tensores relacionais e ROBDDs, mantendo contratos de prova distintos para cada um.
• Estratégia Sensível à Estrutura: Fornece evidência empírica de que a eficiência da verificação é altamente dependente da estrutura do circuito e da ordenação das variáveis. Por exemplo, operandos de somadores intercalados resultam em baixos ranks de tensor (≤3), enquanto operandos divididos resultam em altos ranks (129), tornando estes últimos menos adequados para abordagens baseadas em tensores.
• Diagnóstico de Estado de Reset: Oferece um método para distinguir explicitamente entre dependência real do estado inicial e incerteza transitória em designs síncronos.
• Validação Reproduzível: O artigo inclui um novo suplemento autocontido que valida a construção de tensor train GF(2) exato, medições de rank e testes de função zero em cinco funções de 16 entradas, confirmando a distinção entre cancelamento de paridade e funções zero reais.

Resultos Experimentais
O estudo relata dois conjuntos distintos de evidências:

1. Campanha de Portfólio Histórica (v1.0.0): Este conjunto de dados inclui 89 execuções de casos envolvendo somadores ripple de 2.048 bits, multiplicadores de base polinomial de 128 bits e redes afins.
   • Sucessos: O fluxo completo verificou com sucesso somadores ripple de 2.048 bits (2,87s) e multiplicadores GF de 128 bits (0,80s), superando abordagens baseadas apenas em BDD em casos específicos (ex: somadores de 2.048 bits onde os BDDs falharam em resolver).
   • Limitações: A abordagem atingiu limites de recursos (limites de nós, limites de largura) em somadores ripple de 1.024 bits e redes afins de 1.024 entradas. Os resultados de multiplicação inteira foram limitados a 10 bits devido ao crescimento da ANF e limites de escopo de tensor.
   • Observação: O fluxo completo às vezes incorreu em overhead comparado à seleção direta do motor ideal, destacando o compromisso entre automação e eficiência.
2. Novo Suplemento Reproduzível: Um experimento focado em cinco funções de 16 entradas (incluindo paridade e multiplicação GF) confirmou que a construção de tensor train e a análise de rank são viáveis para funções pequenas. Validou que uma soma escalar GF(2) de zero não implica uma função zero (cancelamento de paridade), uma distinção corretamente tratada pelo teste de zero do TT.

Significância e Alegações
O artigo enquadra explicitamente sua contribuição como uma avaliação técnica delimitada em vez de uma solução universal.

• Não há Superioridade Universal: Os resultados não sustentam a afirmação de que redes de tensores são superiores a todos os outros métodos. Em vez disso, apoiam uma "estratégia sensível à representação", onde diferentes motores são selecionados com base no domínio matemático (ex: álgebra GF para funções de campo finito de baixo grau, eliminação relacional para cadeias de carry).
• Integração sobre Substituição: O resultado central é a integração bem-sucedida de álgebra exata, eliminação relacional, diagramas de decisão e raciocínio temporal, mantendo seus contratos de prova distintos.
• Limites Explícitos: O autor enfatiza que a implementação atual é limitada a primitivas combinacionais binárias e máquinas síncronas pequenas. Ainda não suporta SystemVerilog geral, semântica de consciência de potência (power-aware), temporização assíncrona ou netlists de escala industrial. O artigo distingue entre "prova" (satisfação exata da obrigação booleana codificada) e "certificação" (que requer uma cadeia de frontend e verificador de prova, ambos notados como trabalhos futuros).

Em resumo, o TensorEQC fornece um framework para combinar múltiplos métodos de verificação exata para lidar com lógica heterogênea, demonstrando que, embora nenhum motor seja universalmente ótimo, um portfólio estruturado pode verificar efetivamente classes específicas de circuitos, identificando claramente suas próprias limitações.