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.

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