Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang, Cunxi Yu

TL;DR

ReVEAL tackles the challenge of verifying heavily optimized multipliers by reverse-engineering their architecture with a domain-specific Graph Neural Network. It introduces critical-cone extraction, word-level feature encoding, and a hierarchical, multi-task GraphSAGE classifier to infer PPG, PPA, and FSA templates, enabling efficient SAT-based equivalence checking against a library of pre-verified templates. The approach integrates seamlessly with existing CA and SAT verification pipelines, delivering substantial runtime and memory improvements over state-of-the-art CA and CA+SAT tools while maintaining robustness on diverse architectures. The work demonstrates practical impact by enabling scalable, verifiable verification of large, optimized multiplier circuits and outlines avenues for extending the framework to other datapaths such as MAC units.

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.

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

TL;DR

ReVEAL tackles the challenge of verifying heavily optimized multipliers by reverse-engineering their architecture with a domain-specific Graph Neural Network. It introduces critical-cone extraction, word-level feature encoding, and a hierarchical, multi-task GraphSAGE classifier to infer PPG, PPA, and FSA templates, enabling efficient SAT-based equivalence checking against a library of pre-verified templates. The approach integrates seamlessly with existing CA and SAT verification pipelines, delivering substantial runtime and memory improvements over state-of-the-art CA and CA+SAT tools while maintaining robustness on diverse architectures. The work demonstrates practical impact by enabling scalable, verifiable verification of large, optimized multiplier circuits and outlines avenues for extending the framework to other datapaths such as MAC units.

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.
Paper Structure (31 sections, 10 equations, 4 figures, 12 tables)

This paper contains 31 sections, 10 equations, 4 figures, 12 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Multiplier Architectures
  4. Graph Neural Networks
  5. Modern SAT Solvers and SAT Sweeping
  6. Problem Formulation
  7. Methodology -- the ReVEAL Framework
  8. Critical Cone Extraction
  9. Word-Level Feature Encoding
  10. Inference of Multiplier Architecture
  11. Directional GraphSAGE Model.
  12. Hierarchical Classification.
  13. Stage 1 - Tree vs. Non-tree Discrimination
  14. Stage 2 - Fine-grained Classification
  15. Multi-task Training Strategy.
  16. ...and 16 more sections

Figures (4)

  • Figure 1: Overview of ReVEAL versus Conventional Tools
  • Figure 2: The Workflow of ReVEAL
  • Figure 3: Example of LSB & MSB cone extraction for a 4-bit multiplier
  • Figure 4: Runtime and memory usage across different "optimization-bitwidths".