Boolean Matching Based on Boolean Unification

We consider the problem of detecting the equivalence of two single-output Boolean functions, considering the permutation and complementation of their inputs, complementation of outputs, and their associated don’t-care sets. This is ofien referred to as the Boolean matching problem. Boolean matching is a verification problem, and it has important applications in logic synthesis problems such as technologymapping /?, ?, ?]. In this paper, we present a new algorithm for solving the Boolean matching problem which is based on Boolean unification and branch-andbound techniques. We have applied this algorithm to the iask of technology-mapping for cell-based designs, and experimental results show that it is an eficient and eflectiue algorithm. Comparisons wiih existing Boolean matching algorithms will be presented.