Compositional Performance Verification of Network-on-Chip Designs

Daniel E. Holcomb and Sanjit A. Seshia. Compositional Performance Verification of Network-on-Chip Designs. IEEE Transactions on Computer-Aided Design of Circuits and Systems, 33(9):1370–1383, 2014.

Download

[pdf] 

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.

BibTeX

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

Generated by bib2html.pl (written by Patrick Riley ) on Sun Jun 21, 2015 12:08:13