Improving branch prediction related WCET abstract interpretation

In this paper we refine a Markovian model previously ap-plied to modelize a subset of dynamic branch predictors re-lated WCET delays, in order to take the finiteness of Branch History Table (BHT) into account. The base of the model allows the modeling of a deterministic or non deterministic automaton or set of automata thanks to a Markovian model. We previously applied this formalism to cache related de-lay and cache related preemption delays [4, 7] and simple dynamic branch prediction[6] with infinite BHT. Now we would like to take into account the finiteness of the BHT in the previous model in order to estimate extend our model of static analysis of Worst Case Execution Time (WCET). For illustration, we chose the case of a dynamic prediction based on a two bit saturating counter, with a LRU policy for replacement policy.