Formal performance analysis for faulty MIMO hardware

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.