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

数字集成电路(IC)是基于被称为时钟的周期信号设计的，该信号使被称为同步电路的集成电路(IC)的组件的操作同步。然而，基于时钟的同步设计的刚性导致所产生的IC在极端环境(例如，非常热/很冷、大的温度波动、高辐射)下发生故障。IC设计的另一种方法是异步范例，通过使用本地分布式握手协议而不是全局同步时钟来实现正确的操作。准延迟不敏感(QDI)异步电路已被证明在极端环境中工作，并且与同步电路相比消耗更低的功率。然而，正确地设计QDI电路更加困难，因为它们的行为要复杂得多，而且不受约束。该项目的目标是开发QDI电路的验证方法，这将产生广泛的影响，使QDI电路能够进行可靠的设计，从而在极端环境和低功率物联网(IoT)应用中更广泛地使用QDI电路，如空间探索、电力工业、汽车工业、无线传感器网络等。该项目将通过转移技术与业界密切合作，并计划在该项目所涵盖的技术领域为学生的职业生涯做好准备。提出的技术方法旨在开发一种系统的证明技术，可用于建立QDI电路与其同步电路的功能等价性。它基于形式验证，其中使用数学证明来确定设计的正确性，或者在设计不正确的情况下发现异常。所提出的方法利用了同步电路更容易设计和验证的事实。因此，为了验证QDI电路，将使用先前验证的同步对应物作为参考。

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.