基于变量排序的乘法器电路验证结果的认证器

Authenticator for Verification Results of Multiplier Circuits Based on Variable Ordering

摘要: 验证算术电路特别是门级乘法器电路的正确性是一项重要的研究，目前最有效的验证方法是结合计算机代数和SAT求解来验证门级整数乘法器。为了增加验证结果的可信度，进一步生成证明证书，使用认证器检查以实用代数演算(PAC)证明格式生成单个证明的正确性。在本文中，我们提出了一种基于变量输入顺序的排序方法，使项充分在内部共享以减少冗余项的分配，从而减少认证器所占内存大小。此外，本文用C++语言重新实现了认证器，将函数封装为类，隐藏内部实现细节，提高代码的可读性和复用性，增强了数据安全性。

Abstract: Verifying the correctness of arithmetic circuits, especially gate-level multiplier circuits, is an important study, and currently the most effective verification method is to combine computer algebra and SAT solving to verify gate-level integer multipliers. To increase the confidence of the verification results, proof certificates are further generated using a certifier to check the correctness of generating individual proofs in Practical Algebraic Computation (PAC) proof format. In this paper, we propose a sorting method based on the order of variable inputs so that items are fully shared internally to reduce the allocation of redundant items, thus reducing the memory size occupied by the authenticator. Inaddition, this paper re-implemented the authenticator in C++, encapsulating the function as a class, hiding the internal implementation details, improving the readability and reusability of the code, and enhancing the data security.