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

기술 요약: TensorEQC – 구조 인식형 동치성 검증 (Structure-Aware Equivalence Checking)

문제 정의
동치성 검증(Equivalence Checking, EC)은 회로의 표현 방식에 매우 민선합니다. XOR가 풍부한 네트워크, 캐리 체인(carry chains), 유한체 곱셈기(finite-field multipliers), 정수 곱셈기와 같은 서로 다른 회로 구조는 각기 다른 검증 접근 방식에 유리한 고유한 구조적 특성을 나타냅니다. 단일 방법론(예: 불 대수, 결정 다이어그램 또는 텐서 네트워크)이 모든 유형의 회로를 보편적으로 지배할 수는 없습니다. 또한, 순차 회로를 검증하기 위해서는 관측 가능한 초기 상태 의존성과 특정 관측 경계 내에서 해소되는 불확실성(특히 리셋 상태와 관련하여)을 구분해야 합니다.

방법론
본 논문은 단일한 모놀리식 솔버가 아닌, 다중 알고리즘 포트폴리오로서 설계된 실행 가능한 연구 워크플로우인 TensorEQC를 소개합니다. 이의 핵심 철학은 엔진이 자신의 정확한 의미론(semantics)에 따라 검증 의무를 완수할 수 있는 경우에만 해당 의무를 처리하고, 그렇지 않으면 해당 의무를 다른 엔진으로 넘기는 것입니다.

이 워크플로우는 세 가지 주요 구성 요소로 이루어집니다:

1. 조합 논리 포트폴리오(Combinational Portfolio): 출력값이 해소되거나 자원 제한에 도달할 때까지 프로세스를 수행하는 순차적 파이프라인입니다. 파이프라인에는 다음이 포함됩니다:
   • 구조적 해싱(Structural Hashing): 지원되는 프리미티브(AND, OR, XOR 등) 하에서 표현 DAG의 동일성을 확립하며, 교환 법칙 정규화(commutative normalization)를 적용합니다.
   • 시뮬레이션(Simulation): 무작위, 전영(all-zero), 전일(all-one) 패턴을 사용한 패킹 시뮬레이션을 통해 부정적 증거(negative witnesses/counterexamples)를 찾습니다.
   • 대수적 정규형(Algebraic Normal Forms, ANF): 불 함수를 GF(2) 상의 다변수 선형 다항식으로 표현합니다. 이는 0이 아닌 다항식으로부터 정확한 부정적 증거를 생성하기 위해 특정 보조정리를 활용합니다.
   • 관계형 텐서 제거(Relational Tensor Elimination): 게이트를 불 인디케이터 텐서(Boolean indicator tensors)로 표현합니다. 이는 만족하는 할당의 존재성을 보존하기 위해 GF(2) 합산(패리티 계산) 대신 불 반링(Boolean semiring) 상의 논리합(disjunction)을 통한 변수 제거를 수행합니다.
   • ROBDD 및 전수 조사 폴백(Exhaustive Fallback): 노드 캡(node caps)이 적용된 순서 결정 이진 다이어그램(Ordered Binary Decision Diagrams)과 작은 서포트(small-support)를 가진 전수 열거를 최종 폴백으로 사용합니다.
2. 텐서 트레인(Tensor Train, TT) 분석: 진리표로부터 정확한 TT 표현을 구축하여 대수적 랭크를 측정하고 zero function 여부를 테스트하는 동반 모듈입니다. 이는 GF(2) 상의 랭크와 실수 상의 랭크를 구분하며, GF(2) 랭크가 현저히 작을 수 있음을 명시합니다.
3. 리셋 분석(Reset Analysis): 명시적 상태 자기 구성(explicit-state self-composition)을 사용하여 초기 상태 의존성을 확인하는 동기식 모듈입니다. 이는 리셋 의존성이 즉시 관찰되는 경우와 특정 수의 "플러싱(flushing)" 사이클 후에 사라지는 경우를 구분합니다.

주요 기여

• 정확한 엔진들의 통합: 구조적 해싱, GF(2) 대수, 관계형 텐서 네트워크 및 ROBDD의 실질적인 통합을 보여주며, 각자의 고유한 증명 계약(proof contracts)을 유지합니다.
• 구조 인식 전략: 검증 효율성이 회로 구조와 변수 순서에 크게 의존한다는 경험적 증거를 제공합니다. 예를 들어, 인터리브드 애더(interleaved adder) 피연산자는 낮은 텐서 랭크(≤3)를 보이는 반면, 분리된(split) 피연산자는 높은 랭크(129)를 보여 텐서 기반 접근법에 부적합함을 입증했습니다.
• 리셋 상태 진단: 동기식 설계에서 진정한 초기 상태 의존성과 과도적 불확실성을 명시적으로 구분하는 방법을 제공합니다.
• 재현 가능한 검증: 5개의 16-입력 함수에 대해 정확한 GF(2) 텐서 트레인 구축, 랭크 측정 및 zero function 테스트를 검증하는 새로운 독립형 보충 자료를 포함하여, 패리티 상쇄와 실제 zero function 간의 구분을 확인했습니다.

실험 결과
연구는 두 가지 별도의 증거 세트를 보고합니다:

1. 역사적 포트폴리오 캠페인 (v1.0.0): 이 데이터셋은 2,048비트 리플 애더(ripple adders), 128비트 다항식 기반 곱셈기, 아핀 네트워크(affine networks)를 포함한 89개의 케이스 실행을 포함합니다.
   • 성공 사례: 전체 플로우는 2,048비트 리플 애더(2.87초)와 128비트 GF 곱셈기(0.80초)를 성공적으로 검증하였으며, 특정 케이스(예: BDD가 해결하지 못한 2,048비트 애더)에서 BDD 전용 접근법보다 우수한 성능을 보였습니다.
   • 한계점: 1,024비트 리플 애더 및 1,024-입력 아핀 네트워크에서 자원 제한(노드 캡, 폭 캡)에 부딪혔습니다. 정수 곱셈 결과는 ANF 성장 및 텐서 범위 캡으로 인해 10비트로 제한되었습니다.
   • 관찰: 전체 플로우는 때때로 최적의 엔진을 직접 선택하는 것보다 오버헤드가 발생하여, 자동화와 효율성 사이의 트레이드오프를 보여주었습니다.
2. 새로운 재현 가능한 보충 자료: 5개의 16-입력 함수(패리티 및 GF 곱셈 포함)에 대한 집중 실험을 통해 정확한 텐서 트레인 구축 및 랭크 분석이 소규모 함수에 대해 가능하다는 것을 확인했습니다. 또한, 스칼라 GF(2) 합이 0이라는 것이 반드시 zero function을 의미하지는 않는다는 점(패리티 상쇄)을 검증하였으며, TT zero-test가 이를 올바르게 처리함을 확인했습니다.

의의 및 주장
본 논문은 자신의 기여를 보편적인 솔루션이 아닌 **범위가 한정된 기술적 평가(scoped technical own assessment)**로 명시적으로 규정합니다.

• 보편적 우월성 없음: 결과는 텐서 네트워크가 다른 모든 방법보다 우월하다는 주장을 뒷받침하지 않습니다. 대신, 수학적 도메인(예: 저차수 유한체 함수를 위한 GF 대수, 캐리 체인을 위한 관계형 제거)에 따라 서로 다른 엔진을 선택하는 "표현 민감형 전략"을 지지합니다.
• 대체가 아닌 통합: 핵심 결과는 정확한 대수, 관계형 제거, 결정 다이어그램 및 시간적 추론을 유지하면서도 각각의 증명 계약을 별도로 유지하며 성공적으로 통합했다는 점입니다.
• 명시적 경계: 저자는 현재 구현이 이진 조합 프리미티브 및 소규모 동기식 머신에 국한되어 있음을 강조합니다. 이는 아직 일반적인 SystemVerilog, 전력 인지 세맨틱스(power-aware semantics), 비동기 타이밍 또는 산업 규모의 넷리스트를 지원하지 않습니다. 또한 본 논문은 "증명(encoded Boolean obligation의 정확한 만족)"과 "인증(검증된 프런트엔드 및 증명 체인이 필요한 과정)"을 구분하며, 후자는 향후 과제로 남겨두었습니다.

요약하자면, TensorEQC는 이질적인 로직을 처리하기 위해 여러 정확한 검증 방법을 결합하는 프레임워크를 제공하며, 단일 엔진이 보편적으로 최적일 수는 없지만 구조화된 포트폴리오가 특정 회로 클래스를 효과적으로 검증하는 동시에 자신의 한계를 명확히 식별할 수 있음을 보여줍니다.