功能验证用以保证集成电路RTL级或更高级设计满足功能规范,从而保证集成电路设计的功能正确性。随着信息技术的深入发展,集成电路的功能复杂度不断提高,功能验证已经成为了制约集成电路设计验证过程的瓶颈。模拟验证与形式化验证是功能验证的两种基本方法。半形式化验证技术结合了模拟验证与形式化验证的优点,克服了模拟验证完备性差与形式化验证容易产生状态爆炸的缺点,因而得到了越来越广泛的应用。根据半形式化验证中功能模型的来源,半形式化验证可以分为基于电路设计的半形式化验证与基于功能规范的半形式化验证。前者基于电路设计自动提取功能模型,具有自动化程度高的优点,但是其具有拓展性差、无法实现自动的行为检测以及功能覆盖率度量困难的天然缺陷。后者基于待测设计的功能规范提取功能模型,该方法能够完全独立于电路设计,不关注电路设计内部的实现细节,具有拓展性好、能够实现自动的行为检测与功能覆盖率度量准确等特点,更加适合于大规模/超大规模集成电路设计的功能验证。本文以基于功能规范的半形式化验证为立足点,突破了完备高效的功能模型提取建立、完备高效的自动测试激励生成、自动的功能行为检测以及功能覆盖率的度量等关键技术。论文的创新点以及研究工作包括:1.提出了基于实体状态转移的功能点模型和它的测试空间/全局状态机覆盖率度量方法。该功能模型能够对电路的功能行为与内部结构进行统一描述,从而保证了该模型的完备性与拓展性。基于实体状态转移的功能点模型包含功能点层与实体层两部分,功能点层基于阶段转移关系图模型（STG）对电路设计的功能点进行描述,实体层通过精简的有限状态机对电路内部各个并行工作的功能部件进行描述。本文通过形式化方法证明了该模型的完备性与简洁性,并对典型benchmark目标电路完成了功能点模型的建立。实验表明,对于大规模电路设计,采用基于实体状态转移关系的功能点模型进行功能描述,能够有效避免描述电路内部巨大的状态空间,从而具有良好的简洁性与拓展性。2.本文提出了基于实体状态转移功能点模型的测试空间全覆盖的自动测试向量生成（Automatic Test Pattern Generation,ATPG）算法。该ATPG算法采用改进的Backjumping算法,结合基于功能属性的阶段转移关系测试空间覆盖策略,完备地覆盖了每个功能点的测试空间。最终,通过对包含数据密集型与控制复杂型benchmark目标电路的验证表明,使用该ATPG算法能够平均提高9%的阶段覆盖率与9%的阶段转移关系覆盖率,而对于状态转移关系的测试空间覆盖率的提升则有23%。3.提出了以全局状态机覆盖率为导向的功能点并行调度策略。该策略以基于实体状态转移的功能点模型所对应的全局状态机覆盖率为导向,调度功能点并发执行从而覆盖全局状态机的全部状态空间。实验结果表明,以全局状态机覆盖率为导向的多功能点并发策略,其获得的全局状态机状态覆盖率是采用带约束的随机测试生成方法的2倍左右,且能够大大加快全局状态机状态覆盖率的收敛速度。相比于文献^[100]的激励生成方法,提出的策略能够提高全局状态机覆盖率的收敛速度至少17倍。同时,实验也证明了该多功能点并发策略与创新点2的ATPG方法能够实现兼容,从而达到更高的代码覆盖率与功能覆盖率。4.本文实现了一个基于实体状态转移的功能点模型的自动化验证平台。该平台具有的主要功能包括:1)集成了创新点2与创新点3所提出的激励生成算法;2)提供简单高效的基于实体状态转移的功能点模型建模图形界面;3)提供可配置的验证设置用以指导自动化验证的过程;4)实现基于功能点模型的自动化验证,包括激励自动加载与功能行为自动检验;5)自动输出模拟结果与覆盖率报告。该平台通过将创新点1-3进行统一集成,实现了基于实体状态转移的功能点模型的高效完备的半形式化功能验证。同时,平台集成的图形界面能够实现方便快捷的功能建模,从而进一步提高了验证效率。采用基于实体状态转移的功能点模型的自动化验证平台,我们对数据通路密集型的电路设计浮点运算器（FPU）与控制通路复杂型的电路设计DMA进行验证并获取了验证结果。结果说明了本文提出的半形式化验证技术与相应的自动化验证平台具有良好的验证完备性,相比传统的人工验证方法平均节约了40%左右的验证时间,且相比于形式化验证技术,我们的半形式化方法能够有效避免状态爆炸。本文提出的半形式化验证技术具有良好的拓展性、通用性与完备性,在工业实用的大规模电路设计的功能验证方面具有良好的应用前景。