Reasoning high-level abstractions from bit-blasted Boolean networks (BNs) such as gate-level netlists can significantly benefit functional verification, logic minimization, datapath synthesis, malicious logic identification, etc. Mostly, conventional reasoning approaches leverage structural hashing and functional propagation, suffering from limited scalability and inefficient usage of modern computing power. In response, we propose a novel symbolic reasoning framework exploiting graph neural networks (GNNs) and GPU acceleration to reason high-level functional blocks from gate-level netlists, namely Gamora, which offers high reasoning performance w.r.t exact reasoning algorithms, strong scalability to BNs with over 33 million nodes, and generalization capability from simple to complex designs. To further demonstrate the capability of Gamora, we also evaluate its reasoning performance after various technology mapping options, since technology-dependent optimizations are known to make functional reasoning much more challenging. Experimental results show that (1) Gamora reaches almost 100% and over 97% reasoning accuracy for carry-save-array (CSA) and Booth-encoded multipliers, respectively, with up to six orders of magnitude speedups compared to the state-of-the-art implementation in the ABC framework; (2) Gamora maintains high reasoning accuracy (>92%) in finding functional modules after complex technology mapping, upon which we comprehensively analyze the impacts on Gamora reasoning from technology mapping.

翻译：从位爆破布尔网络（例如门级网表）中推理高级抽象，能够显著提升功能验证、逻辑最小化、数据通路综合、恶意逻辑识别等任务的效率。传统推理方法主要依赖结构哈希与功能传播，面临可扩展性有限以及现代计算能力利用效率低下的问题。为此，本文提出一种新颖的符号推理框架——Gamora，该框架利用图神经网络（GNN）与GPU加速，从门级网表中推理高级功能模块。相比精确推理算法，Gamora提供了高性能推理，具备对超过3300万节点布尔网络的强可扩展性，以及从简单到复杂设计的泛化能力。为进一步验证Gamora的能力，我们还评估了其在多种工艺映射选项下的推理性能（已知工艺相关优化会使功能推理更具挑战性）。实验结果表明：（1）对于进位保留加法器（CSA）和Booth编码乘法器，Gamora的推理准确率分别接近100%和超过97%，相比ABC框架中的最新实现，加速比最高达六个数量级；（2）在复杂工艺映射后，Gamora在查找功能模块时仍能维持高推理准确率（>92%），并据此全面分析了工艺映射对Gamora推理的影响。