高级检索

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

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

  • 摘要: 组合电路等价性验证是数字集成电路设计自动化(EDA)中的重要部分, 随着算术电路在现代计算机系统中的占比逐渐增多, 传统等价性验证算法在验证多比特算术电路, 尤其是乘法器电路时面临挑战, 针对该问题提出一种基于XOR-Majority Graph(XMG)逻辑表示的组合电路等价性验证算法. 首先将两个待验证电路构建成的联接(Miter)电路进行XMG逻辑重写; 其次在等价性一致的前提下对XMG的节点个数和逻辑深度进行逻辑重写优化; 最后调用布尔可满足性(SAT)求解器和仿真器进行验证, 得到最终等价性验证结果. 实验表明, 该算法相比于ABC, Lingeling等工具在验证时间上实现了平均488.6倍、最高1471.7倍的加速.

     

    Abstract: Combinational equivalence checking is an essential part of electronic design automation (EDA). Modern 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. In the first step, a miter circuit is constructed using an XMG representation of the referenced design and the design to be verified. Then, a functional rewrite is performed on the XMG of the miter, in which the logic level and number of nodes are optimized. Lastly, 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 488.6x CPU time speedup on average.

     

/

返回文章
返回