Efficient Combinational Verification Using Overlapping Local BDDs and a Hash Table

We propose a novel methodology that combines local BDDs with a hash table for very efficient verification of combinational circuits. The main purpose of this technique is to remove the considerable overhead associated with case-by-case verification of internal node pairs in typical internal correspondence based verification methods. Two heuristics based on the number of structural levels of circuitry looked at and the total number of nodes in the BDD manager are used to control the BDD sizes and introduce new cutsets based on already found equivalent nodes. We verify the ISCAS85 benchmark circuits and demonstrate significant speedup over existing methods. We also verify several hard industrial circuits and show our superiority in extracting internal equivalences.