Room 206 (2nd floor, badged access)
13 March 2025 - 14h00
MINOTAuR: a timing-predictable RiscV (CVA6) core
Thomas Carle from IRIT, Toulouse Univ.
invited by Claire MAIZA
13 March 2025 - 14h00
MINOTAuR: a timing-predictable RiscV (CVA6) core
Thomas Carle from IRIT, Toulouse Univ.
invited by Claire MAIZA
Abstract: Real-time systems stand out from conventional computer systems by the existence of temporal constraints that must absolutely be respected. They are generally specified in the form of tasks with associated deadlines. When designing a real-time system, an upper bound for the the worst-case execution time for each task must be determined, which is then which is then used to guarantee compliance with deadlines in the worst-case scenario. For the most critical systems, these bounds are obtained through static analyses, which abstract the possible hardware states during task execution. These techniques, considered mature and used in industry for single-core hardware targets, are based on a number of assumptions. However, running programs on even relatively simple processors can lead to counter-intuitive situations known as timing anomalies, which contradict these assumptions, thereby invalidating the results of the analyses and the guarantees that deadlines will be met.
In this seminar, I'll be presenting our work on the design of a timing anomaly-free processor core based on an existing open source RISC-V core (CVA6). This work is based on the results of Sebastian Hahn and Jan Reineke (univ. Saarland) and in particular on the notion of monotonicity of instruction progress in the pipeline. We extended these results to a more complex core, in particular by allowing instructions to be executed speculatively during branch predictions, and by tolerating a certain degree of parallelism in the execution of the instructions. We have modeled the core and formally proved the absence of timing anomalies, first by hand, then using the Coq proof assistant. Our experimental measurements show that the performance cost of the modifications made on the CVA6 is negligible.
