@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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.},
}