A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study