Analyzing Vulnerability of Asynchronous Pipeline to Soft Errors: Leveraging Formal Verification

作者：Lodhi Faiq Khalid^*; Hasan Syed Rafay; Hasan Osman; Awwad Falah

来源：Journal of Electronic Testing-Theory and Applications, 2016, 32(5): 569-586.

DOI：10.1007/s10836-016-5619-8

• Asynchronous pipelines
• MSMA
• Soft errors
• Formal verification of asynchronous circuits
• Model checking
• nuXmv

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.

• 出版日期2016-10