面向等价性验证的锁存器匹配算法

Latch mapping algorithm for equivalence checking

为了克服现有等价性验证技术中难以精确匹配锁存器的局限性,提出了一种结合多种方法的新型锁存器匹配算法.该算法结合任意模拟、局部二叉判决图、目标模拟3种方法来匹配锁存器,并使用了类似滤波器的思想,任意模拟对锁存器作初步快速匹配,提出的局部二叉判决图技术降低了发生内存爆炸的可能性,目标模拟则针对性地对锁存器作进一步的划分.ISCAS89电路实验结果表明,该算法与模拟和自动测试矢量生成等方法相比,在运行时间、占用内存和匹配精度等方面均体现出有效性,可用于处理较大规模的时序电路验证问题.

A novel latch mapping technique for equivalence checking was proposed to overcome the limit of low accuracy of previous mapping methods. The algorithm combined random simulation, local ordered binary decision diagrams （BDD） and target simulation to do latch mapping. It was a filter-like method, where random simulation was used to do quick mapping, and local BDD and target simulation were alternatively used to do further mapping. The efficiency of the proposed approach was shown through its application to the ISCAS89 benchmark circuits.