Per-flow delay bound analysis based on a formalized microarchitectural model

System design starting from high level models can facilitate formal verification of system properties, such as safety and deadlock freedom. Yet, analyzing their QoS property, in our context, per-flow delay bound, is an open challenge. Based on xMAS (eXecutable Micro-Architectural Specification), a formal framework modeling communication fabrics, we present a QoS analysis procedure using network calculus. Given network and flow knowledge, we first create a well-defined xMAS model for a specific application on a concrete on-chip network. Then the specific xMAS model can be mapped to its network calculus analysis model for which existing QoS analysis techniques can be applied to compute end-to-end delay bound per flow. We give an example to show the step-by-step analysis procedure and discuss the tightness of the results.