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 language | English |
|---|---|
| Title of host publication | 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 |
| Publisher | Institute of Electrical and Electronics Engineers |
| Pages | 198-207 |
| Number of pages | 10 |
| ISBN (Electronic) | 9781509002375 |
| DOIs | |
| Publication status | Published - 30 Nov 2015 |
| Event | ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015) - Austin, United States Duration: 21 Sep 2015 → 23 Sep 2015 |
Conference
| Conference | ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015) |
|---|---|
| Abbreviated title | MEMOCODE 2015 |
| Country | United States |
| City | Austin |
| Period | 21/09/15 → 23/09/15 |
Keywords
- Algebra
- Computational modeling
- Fabrics
- Ports (Computers)
- Reachability analysis
- Semantics
- System recovery