Presentation
ReVEAL: Reverse Engineering of Multiplier Architectures via Graph Learning for Computer Algebra Verification
DescriptionArithmetic circuits, particularly optimized multipliers following logic synthesis, pose significant challenges for formal verification due to the difficulty in reconstructing word-level functional
components. Traditional algebraic reasoning methods struggle with these circuits, as optimizations obscure the original word-level components, making reverse engineering difficult. This hampers the
reconstruction of pre-optimized structures, leading to an inability to effectively mitigate the explosion of vanishing monomials, which is a critical issue for Computer Algebra (CA)-based approaches. Although recent methods integrating SAT sweeping and CA through analytical techniques for adder boundary detection have shown improved performance, they still face computational limitations. To address this, we propose ReVEAL, a novel approach that combines Graph Neural Networks (GNNs) and GPU acceleration with CA to facilitate the reverse engineering of optimized multiplier netlists back to their abstraction-level architectures. ReVEAL enables formal verification by concurrently validating reference templates against the under-test multipliers using modern SAT solvers and SAT sweeping techniques. Experimental results show ReVEAL achieves a 4.90 x speedup, 19.97 x memory reduction compared to state-of-the-art CA tools, and a 13.39 x performance increase over combined SAT + CA methods.
components. Traditional algebraic reasoning methods struggle with these circuits, as optimizations obscure the original word-level components, making reverse engineering difficult. This hampers the
reconstruction of pre-optimized structures, leading to an inability to effectively mitigate the explosion of vanishing monomials, which is a critical issue for Computer Algebra (CA)-based approaches. Although recent methods integrating SAT sweeping and CA through analytical techniques for adder boundary detection have shown improved performance, they still face computational limitations. To address this, we propose ReVEAL, a novel approach that combines Graph Neural Networks (GNNs) and GPU acceleration with CA to facilitate the reverse engineering of optimized multiplier netlists back to their abstraction-level architectures. ReVEAL enables formal verification by concurrently validating reference templates against the under-test multipliers using modern SAT solvers and SAT sweeping techniques. Experimental results show ReVEAL achieves a 4.90 x speedup, 19.97 x memory reduction compared to state-of-the-art CA tools, and a 13.39 x performance increase over combined SAT + CA methods.
Event Type
Networking
Work-in-Progress Poster
TimeSunday, June 226:00pm - 7:00pm PDT
LocationLevel 3 Lobby