Conference paper
Formal Semantics of Predictable Pipelines: a Comparative Study
French Alternative Energies and Atomic Energy Commission1
Embedded Systems Engineering, Department of Applied Mathematics and Computer Science, Technical University of Denmark2
Department of Applied Mathematics and Computer Science, Technical University of Denmark3
University of California at Berkeley4
Computer architectures used in safety-critical domains are subjected to worst-case execution time analysis. The presence of performance-driven microarchitectures may trigger undesired timing phenomena, called timing anomalies, and complicate the timing analysis. This paper investigates pipelines specifically designed to simplify the worst-case execution time analysis (also called predictable pipelines).
We propose formal and executable models of four research-oriented pipelines and one industrial pipeline to validate some of their claims related to their timing behavior. We indeed validate, via bounded model checking, the absence of a type of timing anomalies called amplification timing anomalies, or its potential presence by identifying prerequisite to situations where they can occur.
| Language: | English |
|---|---|
| Publisher: | IEEE |
| Year: | 2020 |
| Pages: | 103-108 |
| Proceedings: | 25th Asia and South Pacific Design Automation Conference |
| ISBN: | 1728141230 , 1728141249 , 9781728141237 and 9781728141244 |
| ISSN: | 21536961 and 2153697x |
| Types: | Conference paper |
| DOI: | 10.1109/ASP-DAC47756.2020.9045351 |
| ORCIDs: | Schoeberl, Martin |
Computer architecture Design automation Microarchitecture Model checking Pipelines Semantics Timing amplification timing anomalies computer architecture formal models formal semantics formal verification performance-driven microarchitectures pipeline processing predictable pipelines real-time systems research-oriented pipelines safety-critical domains safety-critical software timing analysis timing behavior worst-case execution time analysis
