Boolean matching based on Boolean unification

The authors 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 often referred to as the Boolean matching problem. Boolean matching is a verification problem, and it has important applications in logic synthesis problems such as technology-mapping. An algorithm for solving the Boolean matching problem which is based on Boolean unification and branch-and-bound techniques is presented. This algorithm has been applied to the task of technology-mapping for cell-based designs, and experimental results show that it is an efficient and effective algorithm. Comparisons with existing Boolean matching algorithms are presented