A Logic Verification Framework for SFQ and AQFP Superconducting Circuits

Traditional logical equivalence checking (LEC), which plays a major role in the entire chip design process, faces challenges of meeting the requirements demanded by the many emerging technologies that are based on logic models different from the standard complementary metal oxide semiconductor (CMOS). In this article, we propose an LEC framework to be employed in the verification process of superconducting electronics (SCE). Our LEC framework is compatible with the existing CMOS technologies and can also check features and capabilities that are unique to SCE. For instance, the performance of nonresistively biased single-flux quantum (SFQ) circuits benefits from ultradeep pipelining, and verification of such circuits requires new models and algorithms. We, therefore, present the multicycle input dependency circuit model which is a novel model representation of design to explicitly capture the dependency of primary outputs of the circuit on sequences of internal signals and inputs. Embedding the proposed circuit model and several structural checking modules, the process of verification can be independent of the underlying technology and signaling. We benchmark the proposed framework on postsynthesis SFQ and 4-phase adiabatic quantum flux parametron netlists. Results show a comparative verification time of SFQ circuit benchmark, including 16-bit integer divider and ISCAS'85 circuits with respect to the ABC tool for similar CMOS circuits.