采用形式化引擎加速处理器仿真验证收敛的关键技术研究

本项目在国际上首次提出以形式化引擎求解覆盖率轨迹反馈驱动仿真测试向量生成，加速验证收敛。通过研究基于覆盖率的高性能形式化引擎、形式化覆盖率轨迹的一致性归约机制以及覆盖率轨迹实时驱动处理器仿真验证的若干关键技术，优化处理器仿真验证过程，实现加速功能验证收敛的目的。与现有覆盖率驱动技术相比，形式化引擎可在很短时间内求取覆盖率轨迹，避免了建立庞大复杂的覆盖率和仿真测试向量的关系库和推理库，在速度和实现开销上具有优势。本项目的研究突破了现有覆盖率驱动的随机仿真验证和形式化技术与仿真相结合的半形式化验证技术框架，在理论上具有研究价值；同时，项目的前期研究显示，本项目提出的采用形式化引擎加速处理器仿真验证收敛技术在性能上也具有优势，依托本项目实现的验证平台未来将应用在国产处理器的验证工作中。