diff options
Diffstat (limited to 'chapters/schedule.tex')
| -rw-r--r-- | chapters/schedule.tex | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/chapters/schedule.tex b/chapters/schedule.tex index d367e4b..c1bb4c3 100644 --- a/chapters/schedule.tex +++ b/chapters/schedule.tex @@ -108,11 +108,20 @@ slightly different structure of the program. \subsection{Starting Work on Modulo Scheduling} After the proofs about hyperblock scheduling are finished, a natural extension is to work on -implementing modulo scheduling, which entails rearranging instructions in loops. +implementing modulo scheduling, which entails rearranging instructions in loops. This would greatly +improve the performance of Vericert as a whole and it would be the final big HLS specific +optimisation that would need to be implemented to be able to call Vericert a proper HLS tool. +However, as mentioned by \cite[author][tristan10_simpl_verif_valid_softw_pipel], dealing with loops +in CompCert can be very tricky and could therefore be an interesting optimisation to work on but may +also be quite challenging. \subsection{Possible Implementation for Dynamic Scheduling} Another plausible extension to Vericert is adding dynamic scheduling, as an alternative, or in -addition to, static scheduling. +addition to, static scheduling. This would have a benefit of maybe being able to combine static and +dynamic scheduling within one design in a verified manner, which was shown to be effective by +\cite[authoryears][cheng20_combin_dynam_static_sched_high_level_synth], and would also be a good way +to improve the throughput of Vericert on loops that need to be scheduled, especially if these have +complicated memory dependencies that would not be analysed by modulo scheduling. \stopcomponent |