Formal Verification and Synthesis Of Null Conventional Logic Circuits

Abstract

The semiconductor industry has given renewed interest to the asynchronous technology since a number of limiting factors exist in modern synchronous digital systems. NULL Conventional Logic (NCL) is a Delay-Insensitive (DI) clockless paradigm convenient for implementing asynchronous circuits but lacks efficient analysis methods and tools for specification and verification. Based on Delay Insensitive Sequential Process (DISP) specification, this chapter exemplifies application of formal methods by applying Process Analysis Toolkit (PAT) to model and verify behavior of NCL circuits. Some useful constructs (Boolean AND gate, toggle element), are successfully modeled and verified using PAT. The flexibility and simplicity of modeling, simulation and verification show the usefulness and applicability of PAT for NCL circuit design and verification.