Faiq Khalid Lodhi, Syed Rafay Hasan, Osman Hasan and Falah Awwad
Abstract
Glitches due to the secondary neutron particles from cosmic rays cause soft errors in integrated circuits (IC). These soft errors are becoming a major threat in modern sub 45nm ICs with multi-billion transistors. Low-power asynchronous null conventional logic (NCL) is generally used to mitigate these soft errors. However, this technique requires extensive simulations and emulations for careful and complete analysis of the design, which can be costly, time consuming and cannot encompass all the possible input conditions. In this paper, we propose a framework to improve the soft error tolerant asynchronous pipelines by identifying and formally analyzing the vulnerable paths using the nuXmv model checker. The proposed framework translates the design behavior and specification into a state-space model and the potential vulnerabilities against soft errors in the pipeline as linear temporal logical (LTL) properties. These formally specified properties are then verified on the state-space model and in case of failure counterexamples are obtained using the nuXmv model checker. The counterexamples can then further be analyzed to obtain the soft error propagation paths and thus give insights about soft error tolerant approaches to the designers. To validate, this work provides an analysis and comparison of the two state-of-the-art asynchronous pipelines, i.e. soft error tolerant asynchronous pipeline I and II. Formal model and analysis of both the pipelines show that the asynchronous pipeline II is comparatively superior against soft errors.
Methodology
Proposed Methodology
State-Space Modeling
State-space Modeling of NCL Pipeline |
State-space Modeling of Soft Errors |
State-space Modeling of SE Tolerant Asynchronous Pipeline I |
State-space Modeling of SE Tolerant Asynchronous Pipeline II |
State-space Modeling of SE Hardened Asynchronous Pipeline |
nuXmv Model
- 2 bit Asynchronous Pipeline
- 2 bit Asynchronous Pipeline I
- 2 bit Asynchronous Pipeline II
- 4 bit Asynchronous Pipeline
- 4 bit Asynchronous Pipeline I
- 4 bit Asynchronous Pipeline II
- 8 bit Asynchronous Pipeline
- 8 bit Asynchronous Pipeline I
- 8 bit Asynchronous Pipeline II
Contact Information
Faiq Khalid is Post Graduate student of Electrical Engineering at NUST School of Electrical Engineering & Computer Science. He is working on this project in the System Analysis & Verification (SAVE) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.
|
|