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

SHF:Small:GOALI:准延迟不敏感电路的形式等效检查

• 批准号: 1717420
• 负责人: Sudarshan Srinivasan
• 金额: $ 45万
• 依托单位: North Dakota State University Fargo
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-08-15 至 2022-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1717420&HistoricalAwards=false
• 关键词: SHF; Small; GOALI; Formal; Equivalence

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.

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

项目成果

Formal Modeling and Verification of PCHB Asynchronous Circuits

PCHB异步电路的形式化建模和验证

• DOI: 10.1109/tvlsi.2019.2937087
• 发表时间: 2019
• 期刊: IEEE Transactions on Very Large Scale Integration (VLSI
• 作者: Sakib, Ashiq A.;Smith, Scott C.;Srinivasan, Sudarshan K.
• 通讯作者: Srinivasan, Sudarshan K.

Illegal Trojan design and detection in asynchronous NULL Convention Logic and Sleep Convention Logic circuits

• DOI: 10.1049/cdt2.12047
• 发表时间: 2022-09
• 期刊: IET Comput. Digit. Tech.
• 作者: Kushal K. Ponugoti;S. Srinivasan;S. Smith;Nimish Mathure

Exploiting Dual-Rail Register Invariants for Equivalence Verification of NCL Circuits

利用双轨寄存器不变量进行 NCL 电路的等效性验证

• 发表时间: 2020
• 期刊: 63rd IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2020
• 作者: Le, Son;Srinivasan, Sudarshan;Smith, Scott.
• 通讯作者: Smith, Scott.

Automated verification of input completeness for NCL circuits

自动验证 NCL 电路的输入完整性

• DOI: 10.1049/el.2018.6068
• 发表时间: 2018
• 期刊: Electronics Letters
• 影响因子: 1.1
• 作者: Le, S.;Srinivasan, S.K.;Smith, S.C.
• 通讯作者: Smith, S.C.

An Equivalence Verification Methodology for Asynchronous Sleep Convention Logic Circuits

异步睡眠约定逻辑电路的等效验证方法

• DOI: 10.1109/iscas.2019.8702098
• 发表时间: 2019
• 期刊: 2019 IEEE International Symposium on Circuits and Systems (ISCAS
• 作者: Hossain, Mousam;Sakib, Ashiq A.;Srinivasan, Sudarshan K.;Smith, Scott C.
• 通讯作者: Smith, Scott C.