  In this paper, we propose a semi-formal verification framework for
single-flux quantum (SFQ) circuits called VeriSFQ, using the Universal
Verification Methodology (UVM) standard. The considered SFQ technology is
superconducting digital electronic devices that operate at cryogenic
temperatures with active circuit elements called the Josephson junction, which
operate at high switching speeds and low switching energy - allowing SFQ
circuits to operate at frequencies over 300 gigahertz. Due to key differences
between SFQ and CMOS logic, verification techniques for the former are not as
advanced as the latter. Thus, it is crucial to develop efficient verification
techniques as the complexity of SFQ circuits scales. The VeriSFQ framework
focuses on verifying the key circuit and gate-level properties of SFQ logic:
fanout, gate-level pipeline, path balancing, and input-to-output latency. The
combinational circuits considered in analyzing the performance of VeriSFQ are:
Kogge-Stone adders (KSA), array multipliers, integer dividers, and select
ISCAS'85 combinational benchmark circuits. Methods of introducing bugs into SFQ
circuit designs for verification detection were experimented with - including
stuck-at faults, fanout errors, unbalanced paths, and functional bugs like
incorrect logic gates. In addition, we propose an SFQ verification benchmark
consisting of combinational SFQ circuits that exemplify SFQ logic properties
and present the performance of the VeriSFQ framework on these benchmark
circuits. The portability and reusability of the UVM standard allows the
VeriSFQ framework to serve as a foundation for future SFQ semi-formal
verification techniques.
