Equivalence Checking for Superconducting RSFQ Logic Circuits

Equivalence checking is a key component of the verification methodology for digital circuit designs. In this paper, we propose an equivalence checking framework for superconducting rapid single-flux-quantum (RSFQ) logic circuits which include acyclic circuits and bit-slice-based cyclic circuits. It consists of a structure checker and a logic checker. The structure checker is used to check whether the circuit meets the design rules of superconducting RSFQ logic circuits. The logic checker can be used to check whether two RSFQ gate-level circuits have the same logic function. For the logic checker, we propose a logic equivalence checking method based on logic cone partition. The circuit network is simplified layer by layer and iteratively partitioned into logic cones, each of which is verified by the SMT solver. The experimental results show the feasibility of our approach on superconducting RSFQ logic circuits.