A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits
The increasing demand for high-speed, energy-efficient, and miniaturized electronics has led to significant challenges and compromises in the domain of conventional clock-based digital designs, most notably reduced circuit reliability, particularly in mission-critical hardware. At scaled technology...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-01-01
|
| Series: | Journal of Low Power Electronics and Applications |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-9268/14/1/5 |
| _version_ | 1797240473514934272 |
|---|---|
| author | Dipayan Mazumder Mithun Datta Alexander C. Bodoh Ashiq A. Sakib |
| author_facet | Dipayan Mazumder Mithun Datta Alexander C. Bodoh Ashiq A. Sakib |
| author_sort | Dipayan Mazumder |
| collection | DOAJ |
| description | The increasing demand for high-speed, energy-efficient, and miniaturized electronics has led to significant challenges and compromises in the domain of conventional clock-based digital designs, most notably reduced circuit reliability, particularly in mission-critical hardware. At scaled technology nodes, devices are vulnerable to transient or soft errors, such as Single Event Upset (SEU) and Single Event Latch-up (SEL). External radiation, internal electromagnetic interference (EMI), or noise are the primary sources of these errors, which can compromise the circuit functionality. In response to these challenges, the Quasi-Delay-Insensitive (QDI) Null Convention Logic (NCL) asynchronous design paradigm has emerged as a promising alternative, offering advantages such as ultra-low power performance, reduced noise and EMI, and resilience to process, voltage, and temperature variations. Moreover, its unique architecture and insensitivity to timing variations offers a degree of resistance against transient errors; however, it is not entirely resilient. Several resiliency schemes are available to detect and mitigate soft errors in QDI circuits, with approaches based on redundancy proving to be the most effective in ensuring complete resilience across all major QDI implementation paradigms, including NCL, Pre-charge/Weak-charge Half Buffers (PCHB/WCHB), and Sleep Convention Logic (SCL). This research focuses on one such redundancy-based resiliency scheme for QDI NCL circuits, known as the dual-modular redundancy-based NCL (DMR-NCL) architecture, and addresses the absence of formal methods for the verification and analysis of such circuits. A novel methodology has been proposed for formally verifying the correctness of DMR-NCL circuits synthesized from their synchronous counterparts, covering both safety (functional correctness) and liveness (the absence of deadlock). In addition, this research introduces a formal framework for the vulnerability analysis of DMR-NCL circuits against SEU/SEL. To demonstrate the framework’s efficacy and scalability, a prototype computer-aided support tool has been developed, which verifies and analyzes multiple DMR-NCL benchmark circuits of varying sizes and complexities. |
| first_indexed | 2024-04-24T18:07:59Z |
| format | Article |
| id | doaj.art-56025b70a2f0487292f60a0c73e5ea2b |
| institution | Directory Open Access Journal |
| issn | 2079-9268 |
| language | English |
| last_indexed | 2024-04-24T18:07:59Z |
| publishDate | 2024-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Journal of Low Power Electronics and Applications |
| spelling | doaj.art-56025b70a2f0487292f60a0c73e5ea2b2024-03-27T13:48:57ZengMDPI AGJournal of Low Power Electronics and Applications2079-92682024-01-01141510.3390/jlpea14010005A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous CircuitsDipayan Mazumder0Mithun Datta1Alexander C. Bodoh2Ashiq A. Sakib3Department of Electrical and Computer Engineering, Florida Polytechnic University, Lakeland, FL 33805, USADepartment of Electrical and Computer Engineering, Florida Polytechnic University, Lakeland, FL 33805, USADepartment of Electrical and Computer Engineering, Florida Polytechnic University, Lakeland, FL 33805, USADepartment of Electrical and Computer Engineering, Florida Polytechnic University, Lakeland, FL 33805, USAThe increasing demand for high-speed, energy-efficient, and miniaturized electronics has led to significant challenges and compromises in the domain of conventional clock-based digital designs, most notably reduced circuit reliability, particularly in mission-critical hardware. At scaled technology nodes, devices are vulnerable to transient or soft errors, such as Single Event Upset (SEU) and Single Event Latch-up (SEL). External radiation, internal electromagnetic interference (EMI), or noise are the primary sources of these errors, which can compromise the circuit functionality. In response to these challenges, the Quasi-Delay-Insensitive (QDI) Null Convention Logic (NCL) asynchronous design paradigm has emerged as a promising alternative, offering advantages such as ultra-low power performance, reduced noise and EMI, and resilience to process, voltage, and temperature variations. Moreover, its unique architecture and insensitivity to timing variations offers a degree of resistance against transient errors; however, it is not entirely resilient. Several resiliency schemes are available to detect and mitigate soft errors in QDI circuits, with approaches based on redundancy proving to be the most effective in ensuring complete resilience across all major QDI implementation paradigms, including NCL, Pre-charge/Weak-charge Half Buffers (PCHB/WCHB), and Sleep Convention Logic (SCL). This research focuses on one such redundancy-based resiliency scheme for QDI NCL circuits, known as the dual-modular redundancy-based NCL (DMR-NCL) architecture, and addresses the absence of formal methods for the verification and analysis of such circuits. A novel methodology has been proposed for formally verifying the correctness of DMR-NCL circuits synthesized from their synchronous counterparts, covering both safety (functional correctness) and liveness (the absence of deadlock). In addition, this research introduces a formal framework for the vulnerability analysis of DMR-NCL circuits against SEU/SEL. To demonstrate the framework’s efficacy and scalability, a prototype computer-aided support tool has been developed, which verifies and analyzes multiple DMR-NCL benchmark circuits of varying sizes and complexities.https://www.mdpi.com/2079-9268/14/1/5asynchronous logicquasi-delay insensitive (QDI)null convention logic (NCL)error resiliencedesign validation |
| spellingShingle | Dipayan Mazumder Mithun Datta Alexander C. Bodoh Ashiq A. Sakib A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits Journal of Low Power Electronics and Applications asynchronous logic quasi-delay insensitive (QDI) null convention logic (NCL) error resilience design validation |
| title | A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits |
| title_full | A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits |
| title_fullStr | A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits |
| title_full_unstemmed | A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits |
| title_short | A Scalable Formal Framework for the Verification and Vulnerability Analysis of Redundancy-Based Error-Resilient Null Convention Logic Asynchronous Circuits |
| title_sort | scalable formal framework for the verification and vulnerability analysis of redundancy based error resilient null convention logic asynchronous circuits |
| topic | asynchronous logic quasi-delay insensitive (QDI) null convention logic (NCL) error resilience design validation |
| url | https://www.mdpi.com/2079-9268/14/1/5 |
| work_keys_str_mv | AT dipayanmazumder ascalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT mithundatta ascalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT alexandercbodoh ascalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT ashiqasakib ascalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT dipayanmazumder scalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT mithundatta scalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT alexandercbodoh scalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits AT ashiqasakib scalableformalframeworkfortheverificationandvulnerabilityanalysisofredundancybasederrorresilientnullconventionlogicasynchronouscircuits |