Validation of Processor Timing Models Using Cycle-Accurate Timing Simulators

Authors Alban Gruin , Thomas Carle , Christine Rochange , Pascal Sainrat

Thumbnail PDF


  • Filesize: 0.72 MB
  • 12 pages

Document Identifiers

Author Details

Alban Gruin
  • IRIT - Univ. Toulouse 3 - CNRS, France
Thomas Carle
  • IRIT - Univ. Toulouse 3 - CNRS, France
Christine Rochange
  • IRIT - Univ. Toulouse 3 - CNRS, France
Pascal Sainrat
  • IRIT - Univ. Toulouse 3 - CNRS, France

Cite AsGet BibTex

Alban Gruin, Thomas Carle, Christine Rochange, and Pascal Sainrat. Validation of Processor Timing Models Using Cycle-Accurate Timing Simulators. In 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023). Open Access Series in Informatics (OASIcs), Volume 114, pp. 2:1-2:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We propose a workflow to help find errors in the processor models that are used to prove their timing predictability. Recently, several papers have modeled processor cores using formal models that represent how instructions progress through the pipeline in each execution cycle. However, such models grow with the complexity of the cores and they are built by hand, using a description of the core, usually the HDL-level code. Such a task is error-prone, and verifying that the model actually captures the core’s timing behavior is required, otherwise the proofs become useless. Our workflow simulates the execution of benchmark applications using the HDL specification of a core in order to extract timing information as well as other relevant information (e.g. cache miss events, branch mispredictions). This information is used to replay the execution in a simulator of the core timing model, and to determine whether or not the model accurately represents the execution timing of the instructions. To avoid writing the simulator by hand for each new core, or new variation of a core, we developed a compiler that translates the timing model of a core into a C++ program. We evaluated our approach on the open source MINOTAuR core and we show how it enabled us to detect and correct errors in its model.

Subject Classification

ACM Subject Classification
  • Hardware → Simulation and emulation
  • Hardware → Equivalence checking
  • Hardware → Safety critical systems
  • Processor model
  • timing predictability
  • simulator generation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Mihail Asavoae, Belgacem Ben Hedia, and Mathieu Jan. Formal executable models for automatic detection of timing anomalies. In Florian Brandner, editor, 18th International Workshop on Worst-Case Execution Time Analysis,WCET, 2018. Google Scholar
  2. Zhenyu Bai, Hugues Cassé, Thomas Carle, and Christine Rochange. Computing execution times with execution decision diagrams in the presence of out-of-order resources. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2023. Google Scholar
  3. Samira Ait Bensaid, Mihail Asavoae, Farhat Thabet, and Mathieu Jan. Work in progress: Automatic construction of pipeline datapaths from high-level HDL code. In 28th Real-Time and Embedded Technology and Applications Symposium (RTAS), 2022. Google Scholar
  4. Benjamin Binder, Mihail Asavoae, Belgacem Ben Hedia, Florian Brandner, and Mathieu Jan. Is this still normal? putting definitions of timing anomalies to the test. In 27th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), 2021. Google Scholar
  5. Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. In Formal Methods for Industrial Critical Systems, 2014. Google Scholar
  6. Franck Cassez, Pablo Gonzalez de Aledo, and Peter Gjøl Jensen. Wuppaal: Computation of worst-case execution-time for binary programs with uppaal. In Models, Algorithms, Logics and Tools, pages 560-577. Springer, 2017. Google Scholar
  7. Heiko Falk, Sebastian Altmeyer, Peter Hellinckx, Björn Lisper, Wolfgang Puffitsch, Christine Rochange, Martin Schoeberl, Rasmus Bo Sorensen, Peter Wägemann, and Simon Wegener. TACLeBench: A benchmark collection to support worst-case execution time research. In 16th International Workshop on Worst-Case Execution Time Analysis, WCET 2016, July 5, 2016, Toulouse, France, pages 2:1-2:10, 2016. Google Scholar
  8. Alban Gruin, Thomas Carle, Christine Rochange, Hugues Cassé, and Pascal Sainrat. MINOTAuR: A timing predictable RISC-V core featuring speculative execution. IEEE Transactions on Computers, 72(1):183-195, 2022. Google Scholar
  9. Andreas Gustavsson, Andreas Ermedahl, Björn Lisper, and Paul Pettersson. Towards WCET Analysis of Multicore Architectures Using UPPAAL. In 10th International Workshop on Worst-Case Execution Time Analysis, 2010. Google Scholar
  10. Sebastian Hahn, Michael Jacobs, and Jan Reineke. Enabling compositionality for multicore timing analysis. In Proceedings of the 24th international conference on real-time networks and systems, pages 299-308, 2016. Google Scholar
  11. Sebastian Hahn and Jan Reineke. Design and analysis of SIC: a provably timing-predictable pipelined processor core. Real-Time Systems, 56(2):207-245, 2020. Google Scholar
  12. Xianfeng Li, A. Roychoudhury, and T. Mitra. Modeling out-of-order processors for software timing analysis. In 25th IEEE International Real-Time Systems Symposium, 2004. Google Scholar
  13. Michael Platzer and Peter Puschner. Vicuna: a timing-predictable RISC-V vector coprocessor for scalable parallel computation. In 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  14. Jan Reineke, Björn Wachter, Stefan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker. A definition and classification of timing anomalies. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006. Google Scholar
  15. Marc Schlickling and Markus Pister. Semi-automatic derivation of timing models for WCET analysis. SIGPLAN Not., 45(4):67-76, April 2010. Google Scholar
  16. Florian Zaruba and Luca Benini. The cost of application-class processing: Energy and performance analysis of a Linux-ready 1.7-GHz 64-bit RISC-V core in 22-nm FDSOI technology. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 27(11):2629-2640, 2019. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail