Compositional Performance Verification of Network-on-Chip Designs

This paper presents a compositional approach to formally verify quality-of-service properties of network-on-chip 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 s without lemmas is proved inductively in just 75 s when the lemmas are used.