Abstraction-Based Performance Verification of NoCs

We present an approach to formally analyze quality-of-service (QoS) properties of network-on-chip (NoC) designs. To tackle industrial-scale designs, we adopt an abstraction-based approach, where only the nodes of interest in the network are precisely modeled and the rest of the network is abstracted away as sources and sinks of traffic. We give an automatic technique to infer a traffic model, comprising formal models of sources and sinks, from simulation traces derived from software benchmarks. Experimental results demonstrate that the inferred models generalize well and that our abstraction-based approach can accurately verify industrial-scale NoC designs.