乘法器电路验证是算术电路验证领域内的一个重大难题。Gröbner基方法是其中目前最为有效的验证方法之一。基于此方法开发的Amulet程序通过减少中间变量数量提高了验证效率,但是对于大型乘法器,验证速度慢的问题仍存在。本文对Amule...乘法器电路验证是算术电路验证领域内的一个重大难题。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基方法是其中目前最为有效的验证方法之一。基于此方法开发的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.
