Optimal Static Task Scheduling on Reconfigurable Hardware Devices Using Model-Checking

Real-time scheduling for FPGAs presents unique challenges to traditional real-time scheduling theory, since it is similar to, but more general than multi-processor scheduling. In his paper, we address two problems of static task scheduling on a partially runtime reconfigurable FPGA: finding an optimal static schedule for a task graph with the optimization objective of minimizing the total schedule length, and finding a feasible static schedule for a set of periodic tasks within a hyper-period with the objective of meeting all deadlines. We model the multi-tasking system with timed automata and use reachability analysis of the UPPAAL model-checker to explore the design space and find an optimal or feasible schedule