  The advent of data-driven real-time applications requires the implementation
of Deep Neural Networks (DNNs) on Machine Learning accelerators. Google's
Tensor Processing Unit (TPU) is one such neural network accelerator that uses
systolic array-based matrix multiplication hardware for computation in its
crux. Manufacturing faults at any state element of the matrix multiplication
unit can cause unexpected errors in these inference networks. In this paper, we
propose a formal model of permanent faults and their propagation in a TPU using
the Discrete-Time Markov Chain (DTMC) formalism. The proposed model is analyzed
using the probabilistic model checking technique to reason about the likelihood
of faulty outputs. The obtained quantitative results show that the
classification accuracy is sensitive to the type of permanent faults as well as
their location, bit position and the number of layers in the neural network.
The conclusions from our theoretical model have been validated using
experiments on a digit recognition-based DNN.
