Simulation and SAT-based Boolean matching for large Boolean networks

Boolean matching is to check the equivalence of two target functions under input permutation and input/output phase assignment. This paper addresses the permutation independent (P-equivalent) Boolean matching problem. We will propose a matching algorithm seamlessly integrating Simulation and Boolean Satisfiability (S&S) techniques. Our proposed algorithm will first utilize functional properties like unateness and symmetry to reduce the searching space. In the followed simulation phase, three types of input vector generation and checking method will be used to match the inputs of two target functions. Experimental results on large benchmarking circuits demonstrate that our matching algorithm is indeed very effective and efficient to solve Boolean matching for large Boolean networks.