基于模型检测的处理器端到端验证方法

时间：2024-12-23 分类：学术活动

Speaker:	李宇锋博士（中国科学院计算技术研究所）
Time:	2024年12月24日 (周二) 14:30
Venue:	中国科学院软件园区5号楼三层 334报告厅
Abstract:	在复杂处理器验证中，基于模型检测的形式化验证方法通过数学建模和逻辑推理验证系统行为的正确性与安全性，能够有效发现边界情况，成为确保系统质量的重要技术手段。得益于求解器性能的提升，端到端验证模式已被广泛采用。与关注微架构信号层的模块级验证不同，端到端验证通过检验指令在流水线中从译码到提交的完整生命周期，能够更全面地捕捉处理器的整体行为。然而，针对特定于设计的属性构造过程通常繁琐且容易出错，给验证带来挑战。本报告介绍了处理器端到端模型检测的方法，特别是近年来提出的符号化快速错误检测（Symbolic Quick Error Detection, SQED）技术。SQED验证一种不依赖于设计的自一致性通用属性，避免了繁琐的手工构造属性的过程，从而显著提高了处理器模型检测的效率。但是，自一致性通用属性缺乏完备性，即无法覆盖单指令类型的故障（single-instruction bugs）。为此，本报告进一步介绍一种基于语义等价程序执行的符号化快速错误检测方法（Symbolic Quick Error Detection by Semantically Equivalent Program Execution, SEPE-SQED），能够实现对故障类型的完备覆盖。
Bio:	李宇锋博士，2024年6月毕业于中国科学院软件研究所，师从杨秋松研究员，从事形式化方法、模型检测、软硬件验证方向的研究，相关工作发表在DAC、ASP-DAC等EDA领域国际著名学术会议上。2024年7月起任职中国科学院计算技术研究所特别研究助理，合作导师包云岗研究员，负责“香山”高性能开源RISC-V处理器的敏捷形式化验证工作。