@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@ARTICLE{holcomb-tcad14, 
 author={Daniel E. Holcomb and Sanjit A. Seshia},
title={Compositional Performance Verification of Network-on-Chip Designs},
journal={IEEE Transactions on Computer-Aided Design of Circuits and Systems}, 
year={2014}, 
volume={33}, 
number={9}, 
pages={1370-1383},
 abstract={This work presents a compositional approach to formally 
verify quality-of-service (QoS) properties of network-onchip 
(NoC) designs. A major challenge to scalability is the need 
to verify worst-case latency bounds for hundreds to thousands 
of cycles, which are beyond the capacity of state-of-the-art 
model checkers. The scalability challenge is addressed using 
a compositional model checking approach. The overall latency 
bound problem is divided into a number of smaller sub-problems, 
termed latency lemmas. The sub-problems imply the overall 
latency bound, but are easier to prove on account of being 
inductive. A method is presented for computing these lemmas 
based on the topology of the network and a subset of relevant 
state, and the latency lemmas are verified using k-induction. 
The effectiveness of this compositional technique is demonstrated 
on illustrative examples and an industrial ring interconnection 
network. In the ring network, a latency bound that cannot be 
verified in 10,000 seconds without lemmas is proved inductively 
in just 75 seconds when the lemmas are used.},
}