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

[pdf] 

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.},
}