当今片上系统(System-on-chip,SoC)设计复杂度越来越高,很多复杂设计已经无法从寄存器传输级(Register Transfer Level,RTL)开始建模,对高层次行为和体系结构模型的需求越来越迫切,系统级功能验证已经成为影响SoC设计效率和质量的最重要环节。针对SoC系统级功能验证各层巨大差异带来的重复工作多、验证效率低下等突出问题,本文研究SoC高层等价性检验技术,在理论和实践上解决目前高层等价性检验存在的问题。SoC高层等价性检验技术主要采用模拟方法,断言方法和形式化方法。模拟方法主要是通过比较在相同的测试激励下,不同层次设计输出结果是否相同。断言的方法主要是通过验证不同层次设计是否满足相同的功能断言。形式化方法主要利用形式化技术(模型检验,谓词抽象和符号模拟)验证不同层次设计是否完全等价。三类方法目前都面临一些困难。模拟方法通过模拟大量的测试矢量进行验证,开销较大并且无法保证测试的完备性。断言方法的验证质量完全取决于定义断言的质量。形式化方法存在需要设计之间的映射关系和状态空间爆炸等问题。本文首先综述了SoC高层等价性检验技术及相关技术迄今为止的研究进展,对现有SoC高层等价性检验方法进行了分类,介绍了每种方法的研究现状,分析了各种方法的优缺点。最后分析了目前SoC高层等价性检验还存在的问题。本文的研究工作围绕SoC高层等价性检验的关键技术展开,针对目前SoC高层等价性检验中存在的问题,提出了新的算法并取得了如下创新成果:首先,针对模拟方法验证效率较低,验证开销大,无法保证设计完备性等问题,本文提出了一种基于覆盖率指导的模拟等价性检验算法。首先分析了系统级与事务级(Transaction Level Modeling,TLM)的相似性(算法描述,模块划分,数据类型)以及覆盖率在不同层次间的关系,根据分析结果,引入代码覆盖率和功能覆盖率作为高层测试矢量的质量测度。利用复合覆盖率(代码覆盖率和功能覆盖率)在系统级产生高质量测试矢量,并利用该测试矢量模拟系统级与TLM模型,比较观察变量的值是否相等。实验结果表明,该方法能重用高层的验证努力,高效地验证系统级与TLM模型的等价性,同时还能有效地提高模拟方法的验证完备性。其次,针对形式化方法需要设计映射信息和验证效率较低等问题,提出了一种基于深度路径的等价性检验算法。该方法提取系统级模型的带数据通路的有限状态机(Finite State Machines with Data Paths,FSMD),随后提取FSMD中所有深度路径。利用测试矢量生成技术,产生所有深度路径的测试矢量。将输出状态语句插入RTL模型中,利用产生的测试矢量模拟RTL模型,输出对应的深度路径。最后,利用符号模拟和约束求解器验证对应路径的等价性。该方法能够验证无映射信息的设计之间的等价性,同时,只需验证对应的深度路径,避免了盲目的深度路径比较。实验结果表明,该方法相比于目前的基于深度路径的方法,减少了深度路径验证次数,提高了等价性检验效率。再次,针对形式化方法需要设计映射信息和验证效率较低等问题,提出了一种基于机器学习的等价性检验算法。该方法无需提取模型的FSMD,减小了验证开销。将状态输出语句插入系统级与RTL代码中,利用硬件设计开发过程中产生的大量测试数据,模拟系统级与RTL模型,得到FSMD状态序列。利用机器学习技术划分状态序列,得到分类状态集合。根据状态的类别,构造系统级与RTL对应的路径。最后利用符号模拟和约束求解器验证对应路径的等价性。该方法能够有效解决差异巨大设计之间的等价性并能验证无对应信息设计的等价性。利用机器学习技术识别对应的路径,减少盲目的路径比较。实验结果表明,该方法能够高效的验证无映射信息的系统级与RTL设计等价性。最后,针对高级综合调度前后验证效率不高,循环结构需要多次迭代等问题,提出了一种基于共享值图(Shared-Value Graph,SVG)的等价性检验算法。该方法利用割点技术,产生高级综合调度前后设计的潜在互模拟位置,利用SVG验证互模拟位置之间公共变量的等价性。割点技术能够划分大规模设计,验证大规模设计的等价性。通过定义互模拟关系减少自动定理证明器求解的次数,提高验证效率。同时,SVG能够一次性的验证循环结构,避免了进行固定点迭代过程中大量的计算。实验结果表明,该方法能够高效的验证高级综合调度前后设计的等价性。