GrO¨bner基法验证乘法器的设计与实现

当今形式化验证工具在大规模集成电路的设计过程中起着非常重要的作用。最有效的方法是以Gröbner基方法为基本原理,将乘法器电路建模为一组伪布尔多项式,通过Gröbner基来既约由多项式表示的字级规范。本文将基于Gröbner基方法,使用C++语言重新实现验证工具,将整个代码分成多个模块的形式,并利用容器类对变量进行分类存储。实验结果表明:C++语言设计的验证工具不仅可以实现成功,而且也为之后的研究提供了有利的验证工具。

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

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