We present a compositional approach to formally verify quality-of-service (QoS) properties of network-on-chip (NoC) designs. A major challenge to scalability is the need to verify latency bounds for hundreds to thousands of cycles, which are beyond the capacity of state-of-the-art model checkers. We address this challenge by a compositional form of k-induction. The overall latency bound problem is divided into a number of sub-problems, termed latency lemmas. Each latency lemma states that a packet spends a smaller number of cycles at a particular “stage” of progress. We present a partially-automated method of computing these stages based on the topology of the network and a subset of relevant state, and verify the latency lemmas using k-induction. The effectiveness of this compositional technique is demonstrated on illustrative examples as well as an industrial ring interconnection network.
展开▼
