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.

Nyckelord

Deadlock freedom

End-to-end delay bounds

Formal framework

Formal verifications

High-level models

Network calculus

On-chip networks

Step-by-step analysis

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)