A Verification Method for Single-Flux-Quantum Circuits Using Delay-Based Time Frame Model

Takahiro KAWAGUCHI  Kazuyoshi TAKAGI  Naofumi TAKAGI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E98-A   No.12   pp.2556-2564
Publication Date: 2015/12/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E98.A.2556
Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: Logic Synthesis, Test and Verification
Keyword: 
single-flux-quantum circuit,  static timing analysis,  formal verification,  

Full Text: PDF(1.1MB)
>>Buy this Article


Summary: 
Superconducting single-flux-quantum (SFQ) device is an emerging device which can realize digital circuits with high switching speed and low power consumption. In SFQ digital circuits, voltage pulses are used for carrier of information, and the representation of logic values is different from that of CMOS circuits. Design methods exclusive to SFQ circuits have been developed. In this paper, we present timing analysis and functional verification methods for SFQ circuits based on new timing model which we call delay-based time frame model. Assuming that possible pulse arrival is periodic, the model defines comprehensive time frames and representation of logic values. In static timing analysis, expected pulse arrival time is checked based on the model, and the order among pulse arrival times is calculated for each logic gate. In functional verification, the circuit behavior is abstracted in a form similar to a synchronous sequential circuit using the order of pulse arrival times, and then the behavior is verified using formal verification tools. Using our proposed methods, we can verify the functional behavior of SFQ circuits with complex clocking scheme, which appear often in practical design but cannot be dealt with in existing verification method. Experimental results show that our method can be applied to practical designs.