基于指针数组的Gr?bner基方法的优化  

Optimization of Gr?bner Basis Method Based on Pointer Array

作　　者：齐爽 冯天烁 史美琦 江建国[1] 

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

出　　处：《计算机科学与应用》2023年第7期1485-1491,共7页Computer Science and Application

摘　　要：门级整数乘法器电路的验证是形式化验证领域内的一个难题,目前最有效的方法是Grӧbner基方法。在基于此方法的验证过程中,多项式的表示对内存的使用情况有很大的影响。在验证工具Teluma中,多项式表示为单项式的链表。由于链表结点需要同时存储数据元素本身的信息和一个指示其直接后继的信息,这会占用较大的内存空间。针对这一问题,本文对多项式的数据结构进行了优化,采用了动态数组存储单项式,指针数组表示多项式的方法。实验结果表明,该优化方法减少了验证过程中内存的使用。The verification of gate-level integer multiplier circuit is a difficult problem in the field of formal verification, and the most effective method is Grӧbner basis method. In the verification process based on this method, the representation of the polynomial has a great influence on the amount of memory used. In the verification tool Teluma, polynomials are represented as linked list of mono-mials. Because linked list nodes need to store both information about the data element itself and a message indicating its immediate successor, this takes up a large amount of memory space. To solve this problem, this paper optimizes the data structure of polynomials. Dynamic array is used to store monomials and pointer array is to represent polynomials. The experimental results show that the optimization method can reduce memory usage in the verification process.

关 键 词：形式化验证 乘法器 对偶变量 Gr?bner基 指针数组 

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