New approach of exploiting symmetry in SAT-based Boolean matching for FPGA technology mapping

Boolean matching is a key procedure in FPGA technology mapping. SAT-based Boolean matching provides a flexible solution for exploring various FPGA architectures. However, the computational complexity prohibits its application practically, inputs permutation is the bottleneck of SAT-based approach. In this paper, a new approach of exploiting symmetry in PLBs architecture and Boolean function is proposed. The problem of input permutation is transformed to the problem of combination assignment according to our three strategies, which directly generate necessary permutations and only check the satisfiability of these necessary permutations. The instances analysis shows that our approach can greatly reduce the problem scale and improve the performance of SAT-based Boolean matching. More experiments will be done, and more factors will be considered in future work.