NULL Convention Logic (NCL) is a Quasi-Delay Insensitive (QDI) asynchronous design paradigm that aims to tackle some of the major problems synchronous designs are facing as the industry trend of increased clock rates and decreased feature size continues. The clock in synchronous designs is becoming increasingly difficult to manage and causing more power consumption than ever before. NCL circuits address some of these issues by requiring less power, producing less noise and electro-magnetic interference, and being more robust to Process, Voltage, and Temperature (PVT) variations. With the increase in popularity of asynchronous designs, a formal verification methodology is crucial for ensuring these circuits operate correctly. Four automated formal verification methodologies have been developed, three to ensure delay-insensitivity of an NCL circuit (i.e., prove Input-Completeness, Observability, and Completion-Completeness properties), and one to aid in proving functional equivalence between an NCL circuit and its synchronous counterpart. Note that an NCL circuit can be functionally correct and still not be input-complete, observable, or completion-complete, which could cause the circuit to operate correctly under normal conditions, but malfunction when circuit timing drastically changes (e.g., significantly reduced supply voltage, extreme temperatures). Since NCL circuits are implemented using dual-rail logic (i.e., 2 wires, rail0 and rail1, represent one bit of data), part of the functional equivalence verification involves ensuring that the NCL rail0 logic is the inverse of its rail1 logic. Equivalence verification optimizations and alternative invariant checking methods were investigated and proved to decrease verification times of identical circuits substantially. This work will be a major step toward NCL circuits being utilized more frequently in industry, since it provides an automated verification method to prove correctness of an NCL implementation and equivalence to its synchronous specification, which is the industry standard.

Asynchronous design is an alternative to the more widely used synchronous design which allows for the elimination of a global clock network and associated design issues such as clock skew. Uncle is a toolflow that provides automated assistance for transforming a synchronous system specified in Verilog RTL to an asynchronous system. With assistance from Uncle an asynchronous delay-insensitive microprocessor is implemented using NULL Convention Logic (NCL) and verified to function properly. An advantage of asynchronous design is that it can be data-driven. Data-driven design allows specific blocks of logic to only be active when they are needed. Data-driven design is implemented to bypass parts of the asynchronous microprocessor. These parts included the ALU and the peripheral hardware multiplier. This resulted in a reduction of total power consumed and an increase in speed. Overall, it was concluded that asynchronous design with Uncle was a viable alternative to synchronous design.

Pre-Charge Half Buffers (PCHB) and NULL convention Logic (NCL) are two major commercially successful Quasi-Delay Insensitive (QDI) asynchronous paradigms, which are known for their low-power performance and inherent robustness. In industry, QDI circuits are synthesized from their synchronous counterparts using custom synthesis tools. Validation of the synthesized QDI implementation is a critical design prerequisite before fabrication. At present, validation schemes are mostly extensive simulation based that are good enough to detect shallow bugs, but may fail to detect corner-case bugs. Hence, development of formal verification methods for QDI circuits have been long desired. The very few formal verification methods that exist in the related field have major limiting factors. This dissertation presents different formal verification methodologies applicable to PCHB and NCL circuits, and aims at addressing the limitations of previous verification approaches. The developed methodologies can guarantee both safety (full functional correctness) and liveness (absence of deadlock), and are demonstrated using several increasingly larger sequential and combinational PCHB and NCL circuits, along with various ISCAS benchmarks. / National Science Foundation (Grant No. CCF-1717420)

Sleep Convention Logic (SCL) is an emerging ultra-low power Quasi-Delay Insensitive (QDI) asynchronous design paradigm with enormous potential for industrial applications. Design validation is a critical concern before commercialization. Unlike other QDI paradigms, such as NULL Convention Logic (NCL) and Pre-Charge Half Buffers (PCHB), there exists no formal verification methods for SCL. In this thesis, a unified formal verification scheme for combinational as well as sequential SCL circuits is proposed based on equivalence checking, which verifies both safety and liveness. The method is demonstrated using several multipliers, MACs, and ISCAS benchmarks.

No description available.

No description available.

No description available.

Asynchronous design is a possible alternative design methodology that has the ability to alleviate issues associated with clock skew, power dissipation, and process and environmental variability among transistors, issues encountered in typical synchronous design methodologies. This investigation studies the implementation of two asynchronous models of the Texas Instruments MSP430 processor family using a logic system known as Null Convention Logic (NCL). The study also investigates two design styles of NCL: the data-driven and control-driven design styles. This example and others show that although there are tradeoffs in chip area and performance, the control-driven design style is a viable methodology that can lead to designs that are low in energy usage. The openMSP430 processor project is the baseline for the investigation as it is a mature open-source project. Silicon-proven multiple times and fully synthesizable, it parallels the original Texas Instruments family nearly cycle for cycle. UNCLE (Unified NCL Environment) is a toolset used to create comparable implementations of the openMSP430 architecture that are data-driven and control-driven in nature. This investigation shows that the control-driven implementation has a slightly larger chip area due to the complexity of the control path and its effects on the data path. While the control path has a lower area than the data-driven model due to area optimization, the data path of the control-driven version is larger than that of the data-driven model. Because of these issues of complexity in both the control and data paths, the performance of the model suffers as well, degrading from the already poor performance of the traditional data-driven NCL model. Along with the increase in chip area and the decrease in performance, the control-driven model sees a 50.2% average decrease in energy usage as compared to the data-driven model. As with most design choices in engineering, there are tradeoffs when using either design style of NCL. This investigation serves to allow designers to make a well-informed decision when deciding between the two.

No description available.

No description available.