In critical real-time systems, the worst-case execution time (WCET) of software tasks must be statically bounded in order to guarantee that they all satisfy their timing constraints (e.g. deadlines). Obtaining such bounds is challenging due to the complexity of the software and of the acceleration mechanisms implemented in the hardware. Particular behaviors, known as timing anomalies, break some simplifying assumptions for the computation of WCET in single and multi-core processors. Some cores have been designed to implement a pipeline-level property known as monotonicity that guarantees that no timing anomaly can occur in the pipeline. Proving the monotonicity of a pipeline is tedious and error-prone, and so is reading the proof and convincing oneself of its validity. We thus propose to rely on the Coq proof assistant to guarantee the soundness of the proofs. In this paper, we show how the monotonicity property and the standard elements composing a pipeline can be modelled in Coq. Using an example based on an open-hardware RISC-V core from the literature, we introduce the main elements of the proof and discuss their reusability for other cores. We conclude that the model and proofs that we provide can be easily adapted to describe other in-order pipelines of equivalent complexity.

We present MINOTAuR, an open-source RISC-V core designed to be timing predictable, i.e., free of timing anomalies: this property enables a compositional timing analysis in a multicore context. MINOTAuR features speculative execution: thanks to a specific design of its pipeline, we formally prove that speculation does not break timing predictability while sensibly increasing performance. We propose architectural extensions that enable the use of a return address stack and of any cache replacement policy, which we implemented in the MINOTAuR core. We show that a trade-off can be found between the efficiency of these components and the overhead they incur on the die area consumption, and that using them yields a performance equivalent to that of the baseline RISC-V Ariane core, while also enforcing timing predictability.

We present MINOTAuR, a timing predictable open source RISC-V core based on the Ariane core [28]. We first modify Ariane in order to make it timing predictable following the approach used to design the SIC processor [12]. We prove that the instruction parallelism in the Ariane core does not prevent from enforcing timing predictability. We further relax restrictions by enabling a limited amount of speculative execution and we are still able to formally prove that the core is timing predictable. Experimental results show that the performance is reduced by only 10% on average compared to the original Ariane core.