ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers

TL;DR

ReVEAL is a graph-learning-based framework that reverse engineers multiplier architectures to enhance algebraic circuit verification, demonstrating improved scalability and accuracy over traditional methods.

Contribution

It introduces a novel GNN-guided approach for reverse engineering multipliers, enabling scalable and accurate verification of optimized multiplier circuits.

Findings

Improves verification scalability for large multipliers

Achieves higher accuracy than rule-based methods

Integrates seamlessly with existing verification workflows

Abstract

We present ReVEAL, a graph-learning-based method for reverse engineering of multiplier architectures to improve algebraic circuit verification techniques. Our framework leverages structural graph features and learning-driven inference to identify architecture patterns at scale, enabling robust handling of large optimized multipliers. We demonstrate applicability across diverse multiplier benchmarks and show improvements in scalability and accuracy compared to traditional rule-based approaches. The method integrates smoothly with existing verification flows and supports downstream algebraic proof strategies.