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

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

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.

Original languageEnglish
Title of host publication2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
PublisherInstitute of Electrical and Electronics Engineers
Pages198-207
Number of pages10
ISBN (Electronic)9781509002375
DOIs
Publication statusPublished - 30 Nov 2015
EventACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015) - Austin, United States
Duration: 21 Sep 201523 Sep 2015

Conference

ConferenceACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015)
Abbreviated titleMEMOCODE 2015
CountryUnited States
CityAustin
Period21/09/1523/09/15

Keywords

  • Algebra
  • Computational modeling
  • Fabrics
  • Ports (Computers)
  • Reachability analysis
  • Semantics
  • System recovery

Fingerprint

Dive into the research topics of 'Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics'. Together they form a unique fingerprint.

Cite this