Per-flow delay bound analysis based on a formalized microarchitectural model
2013 (English)In: 2013 7th IEEE/ACM International Symposium on Networks-on-Chip, NoCS 2013, IEEE , 2013, 6558411- p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
IEEE , 2013. 6558411- p.
Deadlock freedom, End-to-end delay bounds, Formal framework, Formal verifications, High-level models, Network calculus, On-chip networks, Step-by-step analysis
Engineering and Technology
IdentifiersURN: urn:nbn:se:kth:diva-133871DOI: 10.1109/NoCS.2013.6558411ISI: 000326597500016ScopusID: 2-s2.0-84881414097ISBN: 978-146736492-8OAI: oai:DiVA.org:kth-133871DiVA: diva2:663509
2013 7th IEEE/ACM International Symposium on Networks-on-Chip, NoCS 2013; Tempe, AZ; United States; 21 April 2013 through 24 April 2013
QC 201311122013-11-122013-11-112013-11-29Bibliographically approved