基于XMG的乘法器电路等价性验证算法  

An XMG Based Equivalence Checking Algorithm for Large Bit-Width Multiplier Circuits

作　　者：朱柏成 储著飞[1] 潘鸿洋 王伦耀[1] 夏银水[1] Zhu Baicheng;Chu Zhufei;Pan Hongyang;Wang Lunyao;Xia Yinshui(Faculty of Electrical Engineering and Computer Science(EECS),Ningbo University,Ningbo 315211)

机构地区：[1]宁波大学信息科学与工程学院,宁波315211

出　　处：《计算机辅助设计与图形学学报》2024年第3期443-451,共9页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(61871242);专用集成电路与系统国家重点实验室开放课题(2021KF008).

摘　　要：组合电路等价性验证是数字集成电路设计自动化(EDA)中的重要部分,随着算术电路在现代计算机系统中的占比逐渐增大,传统的等价性验证算法在验证多比特算术电路,尤其是乘法器电路时面临挑战.对此,提出一种基于XOR-Majority Graph(XMG)逻辑表示的组合电路等价性验证算法.首先将2个待验证电路构建成的联接(Miter)电路进行XMG逻辑重写;然后在等价性一致的前提下对XMG的节点个数和逻辑深度进行逻辑重写优化;最后调用布尔可满足性(SAT)求解器和仿真器进行验证,得到最终等价性验证结果.实验结果表明,与ABC,Lingeling等工具相比,所提算法在验证时间上实现了平均489倍、最高1472倍的加速.Combinational equivalence checking is an essential part of electronic design automation(EDA).Mod-ern computers have an increasing proportion of arithmetic logic circuits,which poses challenges for traditional equivalence checking algorithms,especially when checking multi-bit logic circuits.An equivalence checking method based on XOR-majority graph(XMG)is proposed to address this issue.Firstly,a miter circuit is con-structed using an XMG representation of the referenced design and the design to be verified.Secondly,a func-tional rewrite is performed on the XMG of the miter,in which the logic level and number of nodes are optimized.Finally,the Boolean satisfiability(SAT)solver and simulator are used to verify the final equivalence verification result.As compared to tools such as ABC and Lingeling,the algorithm performs 489 times CPU time speedup on average,and a maximum acceleration of 1472 times in validation time.

关 键 词：逻辑综合 等价性验证 乘法器电路 异或-多数逻辑图 

分 类 号：TP391.41[自动化与计算机技术—计算机应用技术]