Design And Implementation Of A Formal Verification Tool And A Prototype Platform Of Reconfigurable Systems

With the development of computing technology, especially the emergence of Field Programmable Gate Arrays (FPGA), dynamic reconfigurable computing has become the focus of both academia and embedded industry. In FPGA-based dynamic reconfigurable computing systems, applications are implemented as hardware circuits. Such systems allow reconfiguring the FPGA with different circuits without stopping the system. So dynamic reconfigurable systems can provide with both computing performance similar to Application Specific Integrated Circuits (ASIC) and programming flexibility similar to software.The design of embedded systems based on dynamic reconfigurable computing technology is facing great challenge due to both the complexity of dynamic reconfigurable system architecture and the functional complexity of the applications deployed on it. The biggest issue that all embedded system designers have to deal with is how to guarantee the correctness of system design at different design stages and different abstraction levels.According to this background, we have developed a complete system verification environment for the design of embedded systems leveraging dynamic reconfigurable computing, which contains two verification tools (or platform) for different design stages. First, a formal verification tool for high abstraction level system models is designed and implemented. The tool uses theories and technologies, such as mathematical formula derivation and model checking, to verify the scheduling algorithms and placing algorithms for dynamic reconfigurable systems, which is to make sure the high-level system design meets the requirements on performance, area and predictability. We have also developed a prototype platform based on the uC/OS-Ⅱ real-time kernel. The prototype platform allows verification of the real-time scheduling policies and HW/SW communication mechanisms in real operating system environments. With the help of the verification environment developed in this thesis, system designers can verify the system design at different design stages, which is useful in ensuring design quality, improving design efficiency and reducing design cost. In this case, the design cycle of embedded systems based on dynamic reconfigurable computing is reduced and the time-to-market of embedded products is shortened.