基于指针操作的乘法器验证程序优化  

Optimization of Multiplication Circuit Verification Program Based on Pointer Operations

作　　者：王晨瑞 江建国[1] 

机构地区：[1]辽宁师范大学数学学院,辽宁 大连

出　　处：《应用数学进展》2024年第8期3666-3676,共11页Advances in Applied Mathematics

摘　　要：乘法器电路验证是算术电路验证领域内的一个重大难题。Gröbner基方法是其中目前最为有效的验证方法之一。基于此方法开发的Amulet程序通过减少中间变量数量提高了验证效率,但是对于大型乘法器,验证速度慢的问题仍存在。本文对Amulet的关键算法进行了进一步优化,通过指针操作对函数进行重写,缩短了验证的时间,并根据实验数据体现了其在大型乘法器验证中的应用优势,为形式化验证技术的未来研究提供了参考。The verification of multiplier circuits is a significant challenge in the field of arithmetic circuit verification. The Gröbner basis method is currently one of the most effective verification methods available. The Amulet program, developed based on this method, improves verification efficiency by reducing the number of intermediate variables. However, for large multipliers, the verification speed remains an issue. This paper further optimizes the key algorithms of Amulet, by rewriting functions through pointer operations, reduces verification time. Experimental results demonstrate its advantages in the verification of large multipliers. It provides a reference for future research in formal verification techniques.

关 键 词：乘法器验证 Gröbner基方法 C语言指针 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]