TY - GEN
T1 - Statistical guarantees of performance for MIMO designs
AU - Kumar, Jayanand Asok
AU - Vasudevan, Shobha
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77956572729&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77956572729&partnerID=8YFLogxK
U2 - 10.1109/DSN.2010.5544281
DO - 10.1109/DSN.2010.5544281
M3 - Conference contribution
AN - SCOPUS:77956572729
SN - 9781424475018
T3 - Proceedings of the International Conference on Dependable Systems and Networks
SP - 467
EP - 476
BT - Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
T2 - 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
Y2 - 28 June 2010 through 1 July 2010
ER -