Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking.