结合半加图的算术电路等价性验证技术

Combining half adder graph for equivalence checking of arithmetic circuits

为了克服现有等价性验证技术难以快速验证复杂算术电路的局限性,提出了一种利用综合引擎分析并再现算术电路优化过程的算法.该算法结合了乘法器的编码方式识别技术、加法电路的半加树提取技术和部分积加法电路的架构识别技术来提取乘法电路的实现结构,以此生成与实现电路结构相似且逻辑正确的网表.针对算术电路结构的相似性,仅分析低位输出的电路架构以降低算法复杂度.实验结果表明,与传统的算术电路验证算法相比,该算法可以明显提高算术电路的验证速度,并且可以直接结合到现有的寄存器传输级(RTL)和门级网表的验证流程中,从而提高了算术电路的验证能力.

A new approach was proposed to improve the overall performance of equivalence checking with complicate arithmetic circuits. The synthesis engine was made to replay the optimizations of arithmetic circuit. The algorithm combines the recognition technique of different coding methods in multiplier, the extraction technique of half adder graph （HAG） in addition circuit, and the recognition technique of half adder tree structure of partial product addition circuit. With the extracted information, the register transfer level （RTL） synthesis engine can generate a gate netlist that is logically correct and structurally similar to the implementation. Due to the similarity of arithmetic circuits, only the lower bits＇ outputs need analyzing, which decreases the algorithm complexity. Compared with the traditional verification algorithms of arithmetic circuits, the proposed algorithm can be easily incorporated into the existing RTL-gate equivalence checking frameworks and increase the robustness of the equivalence checking for arithmetic circuits, thus the verification performance is improved.