Specification and analysis of NCL circuits

Due to a number of existing limiting factors in synchronous circuit design, the semiconductor industry gives renewed interest to the application of asynchronous technology. NCL (NULL Conventional Logic) is a Delay-Insensitive (DI) clockless paradigm convenient for implementing asynchronous circuits. Efficient analysis methods and tools are proposed to specify and verify such DI systems. Based on DISP (Delay Insensitive sequential Process) specification, this paper exemplifies application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify behavior of NCL circuits. A few useful constructs, such as Boolean logic gates, binary half adder and pipeline ring, are successfully modeled and verified by using PAT. The flexibility and simplicity of modeling, simulation and verification show the usefulness and applicability of PAT for NCL circuit design and verification.