SAT-Sweeping Based on XOR-Majority Graph

Combinational equivalence checking is a fundamental aspect of electronic design automation (EDA). However, the intricate interconnections of XOR structures in a circuit pose significant challenges for traditional equivalence checking methods. To address these challenges, this paper proposes an equivalence checking method based on SAT-sweeping for XMG networks. This approach fully exploits the efficiency and compactness of XOR and MAJ logic gates in XMG networks for representing logic functions. It incorporates XMG-specific rewriting optimizations and enhances the traditional SAT-sweeping strategy by introducing a SAT-guided method for generating high-toggle-rate simulation vectors, enabling more efficient verification of internal node equivalence. These improvements collectively enhance the overall verification efficiency. In our experimental results, the final results achieve 2.81× and 2.74× improvement compared to state-of-the-art equivalence checking methods.