SPOCK: Static performance analysis and deadlock verification for efficient asynchronous circuit synthesis

Performance analysis and deadlock verification are two critical issues in asynchronous circuit design, which can be advantageous over the synchronous counterpart in terms of robustness against timing variability, security against side-channel attack, and other benefits. Nevertheless, asynchronous design automation tools are far away from mature. In this paper, we advance the synthesis of quasi-delay insensitive (QDI) circuits of pre-charged half buffer (PCHB) and weak-conditioned half buffer (WCHB) pipelines in three respects. First, static performance analysis (SPA) with linear time complexity is generalized from acyclic to cyclic PCHB and WCHB pipelines. Second, a deadlock verification (DV) algorithm with linear time complexity is proposed for checking PCHB and WCHB pipelines using their four-phase marked graph models. Third, we propose a new simple register circuitry for PCHB and WCHB pipelines that consists of one reset-latch and one buffer-latch and is amenable to circuit minimization. With the above two algorithms, we develop an efficient synthesis flow for buffer-latch minimization while maintaining the system throughput and deadlock-free property. Experimental results show the efficiency of our SPA and DV algorithms and demonstrate the effectiveness of our synthesis method with an average of 37% reduction on the number of buffer-laches. As our SPA and DV algorithms are applicable to arbitrary PCHB and WCHB pipelines and our buffer-latch minimization algorithm is orthogonal to existing synthesis methods such as cut-based technology mapping and slack matching, our methods can be generally useful in the analysis, verification, and synthesis of PCHB and WCHB pipelines.