Statistical guarantees of performance for MIMO designs

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.

Original languageEnglish (US)
Title of host publicationProceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
Pages467-476
Number of pages10
DOIs
StatePublished - 2010
Event2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010 - Chicago, IL, United States
Duration: Jun 28 2010Jul 1 2010

Publication series

NameProceedings of the International Conference on Dependable Systems and Networks

Other

Other2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
Country/TerritoryUnited States
CityChicago, IL
Period6/28/107/1/10

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Statistical guarantees of performance for MIMO designs'. Together they form a unique fingerprint.

Cite this