Boolean matching using binary decision diagrams with applications to logic synthesis and verification

An algorithm for Boolean matching based on binary decision diagrams using a level-first search strategy is presented. This algorithm is generally not restricted to circuits with just a few inputs and can be used for both technology mapping and logic verification. Unlike depth-first and breadth-first strategies, a level-first strategy permits significant pruning of the search space. A set of filters that further improve the performance of the matching algorithm is described. A method of analyzing the effectiveness of a filter is presented, and the various filters are ranked on the basis of their effect/cost ratio. Experimental results on a number of benchmark circuits are presented, comparing the basic matching algorithm with and without the use of various filters. It is shown how the matching algorithm and the filters can be extended to Boolean functions with don´t cares