功能验证是集成电路设计流程中的关键环节。随着设计规模与复杂度的增加，功能验证的难度也在不断提高，其中时序电路的激励生成是验证中的经典难题，尤其是针对设计中难以覆盖的边缘属性或状态（即难达状态）进行激励生成通常需要消耗大量的验证资源。模拟验证和形式化验证是两类主要的功能验证方法。形式化方法不需要输入激励，是一种完备、精确的方法，但处理规模非常有限。模拟方法由于具有良好的可扩展性，一直在设计验证的工业应用中占主导地位，但它不是一种完备的方法，难以覆盖设计中的难达状态。近年来兴起的半形式化方法结合了模拟方法和形式化方法两者的优点，被认为是缓解功能验证难题的有效方法。　　本文针对设计中难达状态的验证，研究了基于路径约束求解的半形式化激励生成方法，取得了以下创新性研究成果:　　1.提出了一种基于路径约束求解的难达状态激励生成方法，通过更确定性的激励生成方式，产生较短的时序激励序列覆盖难达目标状态。　　之前的抽象引导半形式化激励生成方法采用的随机激励生成容易陷入局部循环，难以覆盖到难达状态。本方法建立了一种新的难达状态的半形式化激励生成框架:1）在模拟技术方面，结合了具体模拟和符号模拟技术，利用设计的结构信息提取模拟过程中每个周期的路径约束，通过约束条件的翻转与形式化求解产生新的单周期输入激励，其中每个激励对应于一个候选状态;2）在形式化技术方面，基于设计的数据依赖图提取抽象模型，并在此模型上运用形式化的前像计算获取抽象距离信息。利用抽象距离信息对候选状态进行评估与选择，引导具体模拟过程，快速地覆盖难达目标状态。实验数据表明，相比于基于随机的抽象引导半形式化方法以及工业界广泛应用的约束随机模拟方法，所提方法的目标状态覆盖率分别提高了34.78％和56.52％，所产生的激励序列长度平均分别缩短了37.60％和62.42％。　　2.提出了一种基于时序展开的多周期路径约束激励生成方法，相对于单周期路径约束求解进一步提高了目标状态覆盖率和缩短了时序激励序列长度。　　由于单周期路径约束中内部寄存器值无法在输入激励上直接控制，造成部分难达状态无法覆盖或激励生成效率低下。本方法扩展了第一个创新点的工作，通过提取多周期路径约束进行激励生成，利用动态参数化引用-定值链分析变量之间的数据依赖关系，提取出控制条件中寄存器与原始输入之间的赋值依赖关系，以控制约束条件中内部寄存器值，进一步提高激励生成的效率。实验数据表明，与基于单周期路径约束求解的激励生成方法相比，所提方法产生的激励序列长度平均缩短了38.17％，目标状态覆盖率提高了13.04％;与形式化的有界模型检验(Bounded Model Checking，BMC)方法相比，所提方法在激励序列长度相当的情况下将目标状态覆盖率提高了17.39％。　　3.提出了一种针对可观测性分支覆盖的顺序目标路径约束激励生成方法，有效提高了时序激励生成的可观测性分支覆盖率。　　设计验证中的激励生成通常不考虑可观测性，造成设计漏洞被激励后产生的效果不一定被验证人员观察到，带来验证覆盖率虚高问题。本方法以可观测性分支覆盖评估中执行但未被观测到的分支作为激励生成的目标，将要达到的验证目标分解为多个子目标状态顺序覆盖的问题，采用基于多周期路径约束求解的激励生成方法，在抽象距离的引导下，通过依次覆盖各个子目标状态从而实现目标分支的执行和观测，以达到更高的可观测性分支覆盖率，提高设计验证的质量。实验数据表明，所提方法可以将分支覆盖率和可观测性分支覆盖率之间的差值平均值从5.85％缩减为3.99％，即通过进一步激励生成平均弥补了分支覆盖率数据虚高部分的31.79％。