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

Faiq Khalid Lodhi, Syed Rafay Hasan, Osman Hasan, Falah Awwad

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)569-586
Number of pages18
JournalJournal of Electronic Testing: Theory and Applications (JETTA)
Issue number5
Publication statusPublished - Oct 1 2016


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

ASJC Scopus subject areas

  • Electrical and Electronic Engineering


Dive into the research topics of 'Analyzing Vulnerability of Asynchronous Pipeline to Soft Errors: Leveraging Formal Verification'. Together they form a unique fingerprint.

Cite this