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