TY - JOUR
T1 - Analyzing Vulnerability of Asynchronous Pipeline to Soft Errors
T2 - Leveraging Formal Verification
AU - Lodhi, Faiq Khalid
AU - Hasan, Syed Rafay
AU - Hasan, Osman
AU - Awwad, Falah
N1 - Publisher Copyright:
© 2016, Springer Science+Business Media New York.
PY - 2016/10/1
Y1 - 2016/10/1
N2 - Glitches due to the secondary neutron particles from cosmic rays cause soft errors in integrated circuits (IC) that are becoming a major threat in modern sub 45nm ICs. Therefore, researchers have developed many techniques to mitigate the soft errors and some of them utilize the built in error detection schemes of low-power asynchronous null conventional logic (NCL). However, it 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. These counterexamples can then be further analyzed to obtain the soft error propagation paths and thus give insights about soft error tolerant approaches to the designers. For illustration, this work provides an analysis and comparison of three state-of-the-art asynchronous pipelines. Formal model and analysis of all the pipelines show that the soft error hardened pipeline is comparatively superior against soft errors but at the expense of almost two times area overhead.
AB - Glitches due to the secondary neutron particles from cosmic rays cause soft errors in integrated circuits (IC) that are becoming a major threat in modern sub 45nm ICs. Therefore, researchers have developed many techniques to mitigate the soft errors and some of them utilize the built in error detection schemes of low-power asynchronous null conventional logic (NCL). However, it 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. These counterexamples can then be further analyzed to obtain the soft error propagation paths and thus give insights about soft error tolerant approaches to the designers. For illustration, this work provides an analysis and comparison of three state-of-the-art asynchronous pipelines. Formal model and analysis of all the pipelines show that the soft error hardened pipeline is comparatively superior against soft errors but at the expense of almost two times area overhead.
KW - Asynchronous pipelines
KW - Formal verification of asynchronous circuits
KW - MSMA
KW - Model checking
KW - Soft errors
KW - nuXmv
UR - http://www.scopus.com/inward/record.url?scp=84988310671&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84988310671&partnerID=8YFLogxK
U2 - 10.1007/s10836-016-5619-8
DO - 10.1007/s10836-016-5619-8
M3 - Article
AN - SCOPUS:84988310671
SN - 0923-8174
VL - 32
SP - 569
EP - 586
JO - Journal of Electronic Testing: Theory and Applications (JETTA)
JF - Journal of Electronic Testing: Theory and Applications (JETTA)
IS - 5
ER -