Formal performance analysis for faulty MIMO hardware

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Contribution to journalArticlepeer-review


Sources of noise such as quantization, introduce randomness into register transfer level (RTL) designs of complex systems. In previous work, we introduced a formal approach to compute the performance metrics for these designs with high confidence. We defined the performance metrics as properties in a probabilistic temporal logic. We then used probabilistic model checking to verify these properties for RTL and thereby guarantee the statistical performance. In this work, we enhance our previous approach in order to include the effects of permanent and transient faults that may be present in the lower levels of hardware implementation. We then formally analyze the vulnerability of performance of RTL designs to faults that are present at different locations. If a performance requirement is not met, we employ probabilistic model checking with a diagnostic property that can be used to identify the broad cause of performance degradation. In this work, we describe our entire approach by considering RTL designs corresponding to multiple-input-multiple-output (MIMO) communication systems. We illustrate our enhanced approach on the Viterbi decoder which is a nontrivial component of MIMO system designs.

Original languageEnglish (US)
Article number6016225
Pages (from-to)1914-1918
Number of pages5
JournalIEEE Transactions on Very Large Scale Integration (VLSI) Systems
Issue number10
StatePublished - 2012
Externally publishedYes


  • Discrete-time markov chain (DTMC) models
  • RTL faults
  • multiple-input-multiple-output (MIMO) systems
  • probabilistic model checking
  • register transfer level (RTL) performance estimation
  • reliable hardware

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering


Dive into the research topics of 'Formal performance analysis for faulty MIMO hardware'. Together they form a unique fingerprint.

Cite this