Compositional Performance Verification of Network-on-Chip Designs

作者：Holcomb Daniel E^*; Seshia Sanjit A

来源：IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2014, 33(9): 1370-1383.

DOI：10.1109/TCAD.2014.2331342

• On-chip networks
• quality-of-service
• verification

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.

• 出版日期2014-9