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

Resumen Técnico: TensorEQC – Verificación de Equivalencia Sensible a la Estructura

Planteamiento del Problema
La verificación de equivalencia (EC, por sus siglas en inglés) es altamente sensible a la representación de un circuito. Diferentes estructuras de circuitos —como las redes ricas en XOR, las cadenas de acarreo, los multiplicadores de campos finitos y los multiplicadores enteros— exhiben propiedades estructurales distintas que favorecen diferentes enfoques de verificación. Ningún método único (por ejemplo, álgebra booleana, diagramas de decisión o redes tensoriales) domina universalmente todos los tipos de circuitos. Además, verificar circuitos secuenciales requiere distinguir entre la dependencia del estado inicial observable y la incertidumbre que se resuelve dentro de un límite de observación específico, particularmente con respecto a los estados de reinicio (reset).

Metodología
El artículo presenta TensorEQC, un flujo de trabajo de investigación ejecutable diseñado como un portafolio multialgorítmico en lugar de un único resolvedor monolítico. Su filosofía central es que un motor solo debe dar por cumplida una obligación de verificación si puede hacerlo de acuerdo con su propia semántica exacta; de lo contrario, la obligación se transfiere a otro motor.

El flujo de trabajo consta de tres componentes principales:

1. Portafolio Combinacional: Un pipeline secuencial de motores de verificación que procesa salidas hasta que estas se dan por concluidas o se alcanza un límite de recursos. El pipeline incluye:
   • Hashing Estructural: Establece la identidad de los DAG de expresiones bajo primitivas soportadas (AND, OR, XOR, etc.) con normalización conmutativa.
   • Simulación: Utiliza simulación empaquetada con patrones aleatorios, de todo ceros y de todo unos para encontrar testigos negativos (contraejemplos).
   • Formas Normales Algebraicas (ANF): Representa funciones booleanas como polinomios multilineales sobre GF(2). Utiliza un lema específico para generar testigos negativos exactos a partir de polinomios no nulos.
   • Eliminación de Tensores Relacionales: Representa compuertas como tensores indicadores booleanos. Realiza la eliminación de variables mediante la disyunción sobre el semianillo booleano (para preservar la existencia de asignaciones satisfactorias) en lugar de la suma en GF(2) (que computa la paridad).
   • ROBDD y Fallback Exhaustivo: Utiliza Diagramas de Decisión Binaria Ordenados con topes de nodos y enumeración exhaustiva de soporte pequeño como mecanismos de respaldo finales.
2. Analítica de Tensor Train (TT): Un módulo complementario que construye representaciones TT exactas a partir de tablas de verdad para medir el rango algebraico y probar la existencia de funciones cero. Distingue entre rangos sobre GF(2) y números reales, señalando que los rangos de GF(2) pueden ser significativamente menores.
3. Análisis de Reinicio (Reset): Un módulo sincrónico que utiliza autocomposición de estado explícito para verificar la dependencia del estado inicial. Distingue entre casos donde la dependencia del reinicio es observable inmediatamente y casos donde desaparece tras un número específico de ciclos de "limpieza" (flushing).

Contribuciones Clave

• Integración de Motores Exactos: El trabajo demuestra una integración práctica de hashing estructural, álgebra GF(2), redes tensoriales relacionales y ROBDDs, manteniendo contratos de prueba distintos para cada uno.
• Estrategia Sensible a la Estructura: Proporciona evidencia empírica de que la eficiencia de la verificación depende altamente de la estructura del circuito y del ordenamiento de las variables. Por ejemplo, los operandos de un sumador entrelazados producen rangos tensoriales bajos (≤3), mientras que los operandos divididos resultan en rangos altos (129), haciendo que estos últimos sean menos adecuados para enfoques basados en tensores.
• Diagnóstico de Estado de Reinicio: Ofrece un método para distinguir explícitamente entre la verdadera dependencia del estado inicial y la incertidumbre transitoria en diseños sincrónicos.
• Validación Reproducible: El artículo incluye un suplemento nuevo y autónomo que valida la construcción de tensores train exactos en GF(2), las mediciones de rango y las pruebas de función cero en cinco funciones de 16 entradas, confirmando la distincción entre la cancelación de paridad y las funciones cero reales.

Resultos Experimentales
El estudio reporta sobre dos conjuntos distintos de evidencia:

1. Campaña de Portafolio Histórico (v1.0.0): Este conjunto de datos incluye 89 ejecuciones de casos que involucran sumadores de propagación de acarreo de 2,048 bits, multiplicadores de base polinómica de 128 bits y redes afines.
   • Éxitos: El flujo completo verificó exitosamente sumadores de propagación de acarrio de 2,048 bits (2.87s) y multiplicadores GF de 128 bits (0.80s), superando a los enfoques basados únicamente en BDD en casos específicos (por ejemplo, sumadores de 2,048 bits donde los BDD no pudieron resolver).
   • Limitaciones: El enfoque alcanzó límites de recursos (topes de nodos, topes de ancho) en sumadores de propagación de acarreo de 1,024 bits y redes afines de 1,024 entradas. Los resultados de multiplicación entera se limitaron a 10 bits debido al crecimiento de ANF y los topes de alcance de los tensores.
   • Observación: El flujo completo a veces incurre en sobrecarga en comparación con la selección directa del motor óptimo, resaltando el compromiso entre automatización y eficiencia.
2. Nuevo Suplemento Reproducible: Un experimento enfocado en cinco funciones de 16 entradas (incluyendo paridad y multiplicación GF) confirmó que la construcción de tensor train exacto y el análisis de rango son factibles para funciones pequeñas. Validó que una suma escalar de cero en GF(2) no implica una función cero (cancelación de paridad), una distinción manejada correctamente por la prueba de cero de TT.

Significancia y Reivindicaciones
El artículo enmarca explícitamente su contribución como una evaluación técnica delimitada en lugar de una solución universal.

• Sin Superioridad Universal: Los resultados no apoyan la afirmación de que las redes tensoriales son superiores a todos los demás métodos. En su lugar, apoyan una "estrategia sensible a la representación" donde se seleccionan diferentes motores basados en el dominio matemático (por ejemplo, álgebra GF para funciones de campo finito de bajo grado, eliminación relacional para cadenas de acarreo).
• Integración sobre Reemplazo: El resultado central es la integración exitosa de álgebra exacta, eliminación relacional, diagramas de decisión y razonamiento temporal, manteniendo sus contratos de prueba distintos.
• Límites Explícitos: El autor enfatiza que la implementación actual se limita a primitivas booleanas combinacionales y máquinas sincrónicas pequeñas. Aún no soporta SystemVerilog general, semántica consciente de potencia (power-aware), tiempos asíncronos o netlists de escala industrial. El artículo distingue entre "prueba" (satisfacción exacta de la obligación booleana codificada) y "certificación" (que requiere una cadena de frontend y verificador de pruebas, ambos señalados como trabajo futuro).

En resumen, TensorEQC proporciona un marco para combinar múltiples métodos de verificación exacta para manejar lógica heterogénea, demostrando que, si bien ningún motor es universalmente óptimo, un portafolio estructurado puede verificar eficazmente clases específicas de circuitos mientras identifica claramente sus propias limitaciones.