随着计算机技术的发展,尤其是现场可编程门阵列(FPGA)的出现,使动态可重构技术成为嵌入式领域研究的热点和重点。基于FPGA的动态可重构系统采用硬件电路实现计算功能,并允许在系统执行过程中对FPGA的全部或者部分逻辑资源进行动态的功能变换。因此,动态可重构系统能够提供接近专用电路(ASIC)的计算性能和接近软件的可编程性。动态可重构系统体系结构的复杂性,以及通过动态可重构计算所实现的系统功能的复杂性为基于该技术的嵌入式系统的设计带来了巨大挑战。如何在系统的各个设计阶段,针对不同抽象级别的系统设计验证系统的正确性,是摆在所有系统设计者面前的一个亟待解决的问题。基于这一背景,本文为动态可重构系统的开发设计了一套完整的系统验证环境。这一环境主要包括两个服务于不同设计阶段的验证工具/平台。本文设计并实现了一个面向高抽象级别系统模型的形式化验证工具,这一工具通过数学公式推导、模型检测等理论和技术,对动态可重构系统中的调度算法和放置策略等设计进行验证,以保证系统在性能、面积、可预测性等方面的需求得到满足。此外,本文还设计实现了一个基于uC/OS-Ⅱ实时操作系统的原型平台,该平台允许在实际操作系统环境下,对所采用的实时调度策略、软硬件通信机制等详细设计进行验证,以保证在实际环境下策略或机制设计的正确性。通过设计这样一套完整的动态可重构系统验证环境,使得设计者可以在动态可重构系统开发的不同时期对系统的正确性进行验证,从而保证设计质量,提高设计效率,降低设计成本,减少基于可重构技术的嵌入式系统的开发周期和上市时间。