Formal Semantics of Predictable Pipelines: a Comparative Study

Mathieu Jan, Mihail Asavoae, Martin Schoeberl, Edward A. Lee

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

86 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 25th Asia and South Pacific Design Automation Conference
Number of pages6
PublisherIEEE
Publication date2020
ISBN (Print)978-1-7281-4123-7
DOIs
Publication statusPublished - 2020
Event25th Asia and South Pacific Design Automation Conference - China National Convention Center, Beijing, China
Duration: 13 Jan 202016 Jan 2020
https://aspdac2020.github.io/

Conference

Conference25th Asia and South Pacific Design Automation Conference
LocationChina National Convention Center
CountryChina
CityBeijing
Period13/01/202016/01/2020
Internet address

Cite this

Jan, M., Asavoae, M., Schoeberl, M., & Lee, E. A. (2020). Formal Semantics of Predictable Pipelines: a Comparative Study. In Proceedings of the 25th Asia and South Pacific Design Automation Conference IEEE. https://doi.org/10.1109/ASP-DAC47756.2020.9045351