Field Programmable Gate Arrays (FPGAs) are very popular in today's embedded systems design, on which several computation-intensive tasks can be implemented and executed simutaneously. Hardware tasks (HW task) bring great changes to traditional HW/SW co-design field. The real time scheduling algorithm plays an important role in the real time systems and the schedulability analysis is also a necessary step for real-time application design.Partial Runtime-Reconfigurable (PRTR) FPGAs allow hardware tasks to be placed and removed dynamically at runtime. Hardware task scheduling on PRTR FPGAs brings many challenges to the traditional real-time scheduling theory, which have not been adequately addressed by the research community compared to software task scheduling on CPUs.We design and implement a tool for the simulation and analysis of scheduling algorithms on reconfigrable hardware systems. In order to facilitate the research of reconfigurable hardware systems, this tool abstracts the main features of reconfigurable computing system and enables users to investigate different scheduling algorithms as well as evaluate their performance.In this thesis, we consider two important verification methods:simulation and formal verification, which includes theoretical analysis and model-checking. We propose the simulation principle and time-automata modeling method for the schedulability analysis problem on PRTR FPGAs. Then, the design and implementation of the verification tool VeriTool is presented. We evaluate the performance of the verification methods with VeriTool and show finally the applicable scenarios for each method. |