为提高等价性验证效率,提出了一种利用综合引擎重现算术电路的优化过程算法.算法在单向无环图上计算距离,提取出变量的分组和结合顺序;对不同编码方式的乘法器,识别乘数和被乘数的结合顺序.ZDFV的综合引擎根据这些信息生成与实现电路结构相似且逻辑正确的网表.该算法可以直接结合到现有的寄存器传输级(RTL)和门级网表的验证流程中,从而提高算术电路的验证能力.
A new approach was proposed to improve the overall equivalence checking performance. A synthesis engine was made to replay the optimizations of arithmetic circuit and generate a gate netlist of great similarity. The method calculated the distances on directed acyclic graph, and extracted the operand ordering/grouping from a given implementation gate netlist. Multiplier and multiplicand were distinguished on multiplications with different coding methods. With the extracted information, the register transfer level (RTL) synthesis engine of ZDFV could generate a gate netlist that was logically correct and structurally similar to the implementation gate netlist and thus speeded up the equivalence checking process. The approach can be easily incorporated into existing RTL to gate equivalence checking frameworks and increase the robustness of equivalence checking for arithmetic circuits.