一种避免内存爆炸的组合电路等价性验证方法

A combinational equivalence checking method avoiding memory explosion

割集在组合电路等价性验证中得到了广泛的应用,已有的方法常构造能将整个电路一分为二的割集,虽然这种割集在验证后续节点时可以重用已构建的BDD,但它的排序对大多数后续节点都很差,容易引起内存爆炸问题。本文中的割集只针对要验证等价性的某一对点,避免了上述问题。ISCAS85的实验结果表明了它的有效性。

Cut is used wildly in current combinational equivalence checking methods; most of these methods build a cut that can split the original circuit into two small ones. Although this kind of cut can reuse BDDs that already exist, its ordering is so bad for the following nodes and can easily cause memory explosion. The cut in this article only aims at one pair of nodes and can efficiently avoids such explosion. The results based on ISCAS85 show its efficiency.