Semi-Tensor Product-Based Exact Synthesis for Logic Rewriting

Boolean satisfiability (SAT)-based exact synthesis has made significant progress in recent years, particularly in logic rewriting for the identification of potential subnetwork replacements. However, existing rewriting algorithms suffer from two major drawbacks: 1) inflexibility due to precomputed potential replacement candidates and 2) high-computational complexity of off-the-shelf conjunction normal form (CNF)-based SAT solvers. In this article, we propose a novel semi-tensor product (STP)-based exact synthesis approach for logic rewriting. The STP-based exact synthesis encodes Boolean functions into logic matrices and uses circuit-based all solutions SAT (AllSAT) solver to obtain all optimal replacement candidates with a single pass. Additionally, we improve the subnetwork selection strategy to allow flexible rewriting by selecting the most cost-effective implementation of all optimal candidates. Experimental results, compared with the state-of-the-art logic synthesis tool ABC, show that proposed STP-based exact synthesis reduces 41% runtime on average and solves all instances within a time limit. Moreover, after mapping into 6-LUT FPGA technology and standard cells, we obtain average improvements in the area of 6% and 18%, respectively.