Skip to Content

Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics

Posted on

Authors:

  • Wouda, Sanne
  • Joosten, Sebastiaan J. C.
  • Schmaltz, Julien

Published in: Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE International Conference on pp 198–207

DOI: 10.1109/MEMCOD.2015.7340487

Paper

Abstract:

We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

BibTeX entry:

@inproceedings{Wouda15,
 abstract = {We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.},
 author = {Wouda, Sanne and Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
 bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2015.7340487},
 booktitle = {Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE International Conference on},
 doi = {10.1109/MEMCOD.2015.7340487},
 month = {Sep},
 organization = {IEEE},
 pages = {198--207},
 title = {Process algebra semantics \& reachability analysis for micro-architectural models of communication fabrics},
 year = {2015}
}