## Compositional Performance Verification of NoC Designs

Daniel Holcomb, Alexander Gotmanov, Michael Kishinevsky, and Sanjit A.
Seshia. ** Compositional Performance Verification of NoC Designs**. In * Proceedings of the 10th ACM/IEEE International
Conference on Formal Methods and Models for Codesign (MEMOCODE)*, July 2012.

### Download

### Abstract

We present a compositional approach to formally verify quality-of-service (QoS) properties of network-on-chip (NoC) designs. A major challenge to scalability is the need to verify latency bounds for hundreds to thousands of cycles, which are beyond the capacity of state-of-the-art model checkers. We address this challenge by a compositional form of k-induction. The overall latency bound problem is divided into a number of sub-problems, termed latency lemmas. Each latency lemma states that a packet spends a smaller number of cycles at a particular “stage” of progress. We present a partially-automated method of computing these stages based on the topology of the network and a subset of relevant state, and verify the latency lemmas using k-induction. The effectiveness of this compositional technique is demonstrated on illustrative examples as well as an industrial ring interconnection network.

### BibTeX

@InProceedings{holcomb-memocode12, author = {Daniel Holcomb and Alexander Gotmanov and Michael Kishinevsky and Sanjit A. Seshia}, title = {Compositional Performance Verification of NoC Designs}, booktitle = {Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, month = {July}, year = {2012}, abstract = {We present a compositional approach to formally verify quality-of-service (QoS) properties of network-on-chip (NoC) designs. A major challenge to scalability is the need to verify latency bounds for hundreds to thousands of cycles, which are beyond the capacity of state-of-the-art model checkers. We address this challenge by a compositional form of k-induction. The overall latency bound problem is divided into a number of sub-problems, termed latency lemmas. Each latency lemma states that a packet spends a smaller number of cycles at a particular ``stage'' of progress. We present a partially-automated method of computing these stages based on the topology of the network and a subset of relevant state, and verify the latency lemmas using k-induction. The effectiveness of this compositional technique is demonstrated on illustrative examples as well as an industrial ring interconnection network.}, }