SHF:Small:GOALI:Formal Equivalence Checking for Quasi-Delay-Insensitive Circuits

点击翻译按钮获取中文摘要

Digital integrated circuits (ICs) are designed based on a periodic signal called the clock, which synchronizes the operation of the components of an Integrated Circuit (IC) referred to as synchronous circuits. However, the rigidity of clock-based synchronous design causes the resulting ICs to malfunction in extreme environments (e.g., very hot/cold, large temperature swings, high radiation). An alternate approach to IC design is the asynchronous paradigm, where correct operation is achieved through the use of locally distributed handshaking protocols instead of a global synchronizing clock. Quasi-Delay-Insensitive (QDI) asynchronous circuits have been shown to function in extreme environments and also consume lower power compared to synchronous circuits. However, designing QDI circuits correctly is more difficult, because their behavior is much more complex and unconstrained. The goal of this project is to develop verification methodologies for QDI circuits, which will have a broad impact, enabling reliable design and therefore more widespread usage of QDI circuits in extreme environment and low-power Internet of Things (IoT) applications, such as space exploration, power industry, automobile industry, wireless sensor networks, etc. The project will have close collaboration with industry via transfer technology, and plans to prepare students for a career in the technical fields covered by this project.The proposed technical approach aims to develop a systematic proof technique that can be used to establish the functional equivalence of a QDI circuit with its synchronous counterpart. It is based on formal verification, where mathematical proofs are used to establish correctness of the design, or find anomalies if the design is not correct. The proposed approach exploits the fact that synchronous circuits are much easier to design and verify. Therefore, to verify a QDI circuit, the previously verified synchronous counterpart will be used as the reference.