document: Efficient combinational verification using overlapping local BDDs and a hash table We propose a novel methodology that combines local BDDs -LRB- binary decision diagrams -RRB- 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
doc_bio_tags: O B I O B I I O O B I O O O O O O O O O O B I I O O O B I O O O O O O O O O O O O O O O O O O O O O O O O O B I I O O B I I I O O O B O O O O O B I O O O O O O O O O O O O B I O O O O O B I O O O B O O O O O O O O O O B I I O O O O O O O O O O O O B I I O O O O O O B I
extractive_keyphrases: combinational verification overlapping local bdds hash table internal node pairs internal correspondence based verification heuristics structural levels bdd manager bdd sizes cutsets iscas85 benchmark circuits hard industrial circuits internal equivalences binary decision diagrams
abstractive_keyphrases: combinational circuit verification case-by-case verification formal verification internal correspondence-based verification