系统复杂性继续按照摩尔定律增加,而功能复杂性的增加速度则更加迅猛。为解决复杂性增加的问题,EDA行业提出了通过自动化来实现设计抽象(Design Abstraction)的概念。由于设计生产率的提升速度低于系统复杂性的增速,此时与设计相关的瓶颈已并非设计时间,而是验证时间,即验证瓶颈。为此,人们创建了能够在不同抽象级别上对复杂系统设计进行验证的新型验证语言,例如,高级验证语言SystemC。实践证明SystemC是一种优秀的系统设计描述验证语言,它能够完成从系统级到门级、从软件到硬件、从设计到验证的全部描述。本文阐述了基于SystemC的主要验证方法和相关理论,以及时态逻辑理论和在验证领域中的应用,一方面分析了在动态仿真中已有的基于SystemC时态逻辑属性验证方法存在的不足,改进了动态仿真中时态逻辑属性描述方法,并在此基础上提出了一种属性化简方案,提高了仿真性能;另一方面实现了SystemC电路的可达性分析,及基于可达性分析的时态逻辑属性验证算法,并通过实验证实了文中提出的属性验证方法的有效性。本文的主要贡献如下:1.从动态仿真的角度来验证时态逻辑属性,本文在R.Dechsler等人提出的基于SystemC属性检查器验证方法的基础上进一步研究,分析了已有属性描述方法的不足,提出了一种改进的属性化简的描述方法,并通过实验验证了改进方案的有效性。2.从可达性分析的角度来验证时序电路的时态逻辑属性,针对基于SvstemC描述的门级电路,提出了时序电路可达性分析的实现方案。主要包括门级时序电路信息提取方法和时序状态转移函数构建方法的实现,其中时序状态转移函数通过bdd来构造,然后通过对状态转移函数的bdd表示进行求解来获取状态间的转移关系。最后通过4个基本时序电路实例来说明可达性分析方案的可行性。3.在可达性分析的基础上,进一步验证时序电路的时态逻辑属性。时态逻辑属性仍然采取前面提到的动态仿真方法中属性描述方法。结合属性描述方法,提出了一种时态属性验证方案并实现了该算法,并将该属性验证算法应用于基于SystemC描述的时序电路等价性问题上,将时序等价问题转换成时态逻辑验证问题来完成等价性验证问题,并通过实例进行说明验证算法的有效性。