CN115544926B 一种基于xmg组合电路的等价性验证装置及方法 （宁波大学）

106005.一种基于XMG组合电路的等价性验证装置及本发明公开的基于XMG组合电路的等价性验证装置包括依次连接的输入读取模块、构建适用于XMG网络的XMG内部XOR节点的常量替换算法，将XMG内部的XOR节点及其子电路看作为本发明在CPU计算时间和内存占用方面分别减少了3097.03倍和40.7%，既能降低等价性验证时2所述的输入读取模块，用于将输入的待验证等价性的两个电路的信息文所述的构建Miter电路模块，用于根据所述的输入读取模块得到的两个电路的解析的所述的常量替换算法模块，用于对XMG网络结构的Miter电路中内部XOR节点进行常数所述的等价性判断模块，用于根据最后输出XMG网络的XOR节点数，判2)构建Miter电路模块根据输入读取模块得到的两个电路的解析的数据分别构建电路4)常量替换算法模块对XMG网络结构的Miter电路中内部XOR节点进行常数替换，输出3.根据权利要求2所述的一种基于XMG组合电1)的具体过程为：输入读取模块读取蕴含两个电路信息的aig文件并存储，得到AIG_4.根据权利要求2所述的一种基于XMG组合电路的等价性验5.根据权利要求2所述的一种基于XMG组合电6.根据权利要求2所述的一种基于XMG组合电路的等为0则判断两个电路等价，若节点数不为0则继续交给SAT求解器求解并判断两个电路是否3[0001]本发明涉及组合电路等价性验证领域，具体是一种基于XMG组合电路的等价性验有序二元决策图(reducedorderedbinarydecisiondiagram,ROBDD)等。正则性指的是检测电路的正则性表示是否相同即可判定电路是否等价。但这种方法仅适用于小规模电Satisfiability,SAT)求解器的形式化方法来判定[0006]本发明解决上述技术问题所采用的技术方案为：一种基于XMG组合电路的等价性[0008]所述的构建Miter电路模块，用于根据所述的输入读取模块得到的两个电路的解4[0010]所述的常量替换算法模块，用于对XMG网络结构的Miter电路中内部XOR节点进行[0014]2)构建Miter电路模块根据输入读取模块得到的两个电路的解析的数据分别构建[0016]4)常量替换算法模块对XMG网络结构的Miter电路中内部XOR节点进行常数替换，[0023]1)传统的等价性验证工具对于9bit的三输入加法乘法器出的基于XMG组合电路的等价性验证装置及方法极大地提高了等价性验证效率，同时降低5明提出的基于XMG组合电路的等价性验证装置及方法降低了等价性验证的难度，在可满足解的质量和计算速度方面提升明显：本发明提出的基于XMG组合电路的等价性验证装置及出的基于XMG组合电路的等价性验证装置及方法极大地提高了等价性验证效率，同时降低[0029]图4为实施例2中步骤4)的对XMG网络结构的Miter电路中内部XOR节点进行常数替示。构建Miter电路模块20用于根据输入读取模块10得到的两个电路的解析的数据分别构换模块30用于将构建的Miter电路转换成XMG网络结构。常量替换算法模块40用于对XMG网[0034]对于两个输入变量的位宽为8bit的待验证算术电路(a+b)c和ac+bc的等价性验证节点之间的连接关系以及两个电路的原始输入端和原6[0036]2)构建Miter电路模块根据输入读取模块得到的两个电路的解析的数据分别构建[0039]4)常量替换算法模块对XMG网络结构的Miter电路中内部XOR节点进行常数替换，[0040]5)等价性判断模块根据最后输出XMG网络的XOR节点数，[0041]本发明所提出的基于XMG组合电路的等价性验证装置及方法，相比于传统性能最优的等价性验证工具ABC(MishchenkoA,ChatterjeeS,BraytonR,etal.Improvementstocombinationalequivalencechecking[C]//2006IEEE/ACMInternationalConferenceonComputerAidedDesign:IEEE,2006:836_843.)，在计算速度和占用内存置及方法与传统性能最优的等价性验证工具的性7提出的基于XMG组合电路的等价性验证装置及方法降低了等价性验证的难度，在可满足解的质量和计算速度方面提升明显：本发明提出的基于XMG组合电路