基于动态数组的加法器重写优化算法

Adder Rewriting Optimization Algorithm Based on Dynamic Array

摘要: 乘法器电路验证是算术电路验证领域内的一个重大难题。当前最有效的代数验证方法是Gröbner基方法。基于此方法提出的加法器重写算法是一项重大创新，但识别加法器的过程需要穷举遍历电路变量，并且十分低效。为了解决这一问题，本文对加法器重写算法进行了优化，使用动态数组存储搜索加法器所需的门变量，并以逆拓扑序的顺序来遍历，从而消除了冗余。实验结果表明，结合动态数组来识别加法器能够有效提高Gröbner基的生成效率和验证速度。

Abstract: Verification of multiplier circuits is an important problem in the field of arithmetic circuit verification. Currently, the most effective algebraic verification method is the Gröbner basis method. The adder rewriting algorithm proposed based on Gröbner basis method is a major innovation, but the process of identifying requires exhaustive traversal circuit variables and is very inefficient. To solve this problem, this paper optimizes the adder rewriting algorithm, using a dynamic array to store the gate variables required to search the adders and traverse in reverse topological order, which eliminates redundancy. Experimental results show that combining the dynamic array to identify the adders can effectively improve the generation efficiency of Gröbner basis and the verification efficiency.