WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction

Autor: Armel Mangean, Sébastien Faucou, Mikaël Briday, Jean-Luc Bechennec

Publikováno v: Verification and Evaluation of Computer and Communication Systems. VECoS 2017
Verification and Evaluation of Computer and Communication Systems. VECoS 2017, Aug 2017, Montréal, Canada. pp.64--78, ⟨10.1007/978-3-319-66176-6_5⟩
Lecture Notes in Computer Science ISBN: 9783319661759
VECoS

In this paper, we investigate the case for model checking in the WCET analysis of pipelined processors with dynamic branch and target prediction. We consider a microarchitecture inspired by the e200z4 Power 32-bit architecture, with an instruction ca

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d0e81c8076df36d0686017006dad65e
https://hal.archives-ouvertes.fr/hal-01713094