SystemC是一种软硬件协同设计语言，可以完成从系统级(System Level)到寄存器传输级(Register Transfer Level，RTL)的设计。相比软硬件使用不同语言的设计模式，使用SystemC进行系统设计可以大大缩短开发周期。近年来，随着嵌入式系统，尤其是片上系统(System on a Chip, SoC)的广泛应用，SystemC语言越来越受开发者的青睐。很多嵌入式系统都是安全攸关的，例如航空航天系统、医疗卫生系统、交通控制系统等等，这些系统失效将导致灾难性的后果，因此需要极高的可靠性。目前对嵌入式系统的验证仍大量依赖系统仿真，但仿真方法不能完全覆盖系统运行的所有情况，因而系统的可靠性难以得到有效的保障。形式化方法则可以覆盖系统运行的所有情况，其中模型检测方法以其自动化的特点最受欢迎。但是模型检测方法存在状态空间爆炸问题，验证的规模受到限制。本研究旨在为SystemC程序的验证提供形式化的理论和方法支持，以提高验证效率。　　本论文的研究内容涉及SystemC寄存器传输级程序的验证和系统级程序的验证两个方面。在SystemC寄存器传输级程序验证方面，本文研究了基于通用符号轨迹求值(Generalized Symbolic Trajectory Evaluation，GSTE)的对称归约方法来提高程序验证效率。在SystemC系统级程序验证方面，本文首先研究了一个系统级SystemC子集的操作语义，然后基于此语义实现了SystemC源程序到卫迁移系统(Guarded Assignment System)的自动转换工具，并研究了基于符号化模型检测的偏序归约算法来提高程序验证效率。　　本论文的成果和创新性贡献主要有以下几点.　　一、针对寄存器传输级模型，提出了一种基于通用符号轨迹求值的对称归约方法。本方法是通用符号轨迹求值与对称归约方法结合的首个研究。对称归约的过程采用了定理证明的方法:首先，将性质的可满足性作为最终目标;其次，使用分解规则将最终目标替换成多个子目标，每个子目标存在对称关系。再次，调用GSTE方法验证其中一个子目标。最后，通过对称规则归约其他子目标。　　二、用卫迁移系统定义了一个系统级SystemC子集的操作语义，并完成了SystemC系统级程序到卫迁移系统的自动转换工具SC2VVM，从而实现了用VERDS模型检测工具自动验证SystemC程序。我们定义了一个转换函数，将SystemC的语句映射到迁移的集合。基于迁移系统的特性，我们简化了SystemC调度器，将时间消耗改为递减的方式，并证明修改后的语义与原始语义等价。　　三、针对SystemC系统级模型，提出了一种基于符号模型检测的偏序归约算法，根据并发系统中进程之间的依赖关系不同程度地提高验证效率。此算法也可用于验证一般的并发系统。SystemC进程由若干个不可中断的原子迁移块组成，我们基于这些原子迁移块，通过布尔公式的操作将偏序归约的条件应用到算法中。在一般的并发系统中，一条迁移就是一个原子操作，因此适用SystemC的算法。