集成电路是现代信息产业和信息社会的基础,随着网络化和知识经济浪潮的到来,集成电路系统已经渗入到了我们生活中的各个领域,而随着芯片复杂度的增大,设计出错的可能性也越来越大,因此对系统正确性的验证也越发必要。超大规模集成电路(VLSI)的设计与开发需要投入大量的财力、物力、人力等资源,对一个已经开发完成的电路系统再进行错误测试和修复将付出巨大的代价,所以,产业界更倾向于在设计初期尽可能发现错误并进行纠正。集成电路系统的验证方法有传统方法(模拟、仿真和测试)和近些年提出的形式化验证方法。由于电路系统规模的日益复杂,传统验证方法耗费大量的系统资源还不能保证设计的正确性,于是学术界和产业界目前更关注于形式化方法的研究。本文着重研究了形式化验证方法中的等价性验证方法。等价性验证是形式化方法中适合于集成电路系统验证的方法之一,电路系统设计的等价性验证用来验证两个电路逻辑功能是否一致。随着电路系统复杂性的增大,验证过程中电路可能存在未完成部分或者验证人员有意忽略部分,这部分电路称之为未知模块。集成电路系统按照是否存在未知模块分为完全实现电路系统和部分实现电路系统;按照电路结构不同,可分为组合电路系统和时序电路系统两种。本文提出了一种针对部分实现的时序电路系统等价性验证的有效方法。该方法首先将部分实现时序电路划分成为逻辑锥,通过把逻辑锥中的时序单元做时间帧展开使之内部成为组合电路结构,再用可满足性的方法进行验证。此方法中使用四值逻辑技术对电路中的未知模块部分进行处理。该算法扩充了对部分实现时序电路等价性验证的研究,将时序电路的验证转化成组合电路验证,有效增强了错误检测能力,可以缩减算法的验证时间。