近日，中国科学院软件研究所基础软件国家工程研究中心团队的两篇论文被国际电子设计自动化（EDA）领域顶级会议Design Automation Conference（DAC 2024, CCF-A类）录用。研究成果聚焦于硬件模型检测领域，助力了处理器检测方法的改进和检测算法的性能提升。

论文SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution第一作者博士生李宇锋，通讯作者杨秋松研究员。论文提出了一种基于通用属性验证的处理器模型检测方法SEPE-SQED，改进了符号化快速错误检测（Symbolic Quick Error Detection, SQED）一类方法的不完备性问题。

SQED类方法通过断言原始指令与其操作码相同的复制指令在相同处理器模型中的执行结果须一致，构造了一种不依赖于微架构设计的通用属性——自一致性属性，解决了处理器形式验证中需要属性定制的问题，这类方法可以极大地降低处理器模型检测的门槛。然而，自一致性属性还不具有完备性，缺乏对于一类源于单指令故障引起的错误的覆盖，会导致对于这类错误的检测出现结果假阳性，进而需要仿真或者其它形式化方法的配合。

针对上述问题，论文提出的SEPE-SQED方法泛化了SQED中的自一致性属性，扩展到比较原始指令和其语义等价的指令序列在处理器模型中的执行结果。由于单指令类型的错误不会同效果地影响到原始指令和其语义等价的指令序列，因此避免了检测结果出现假阳性。此外，SEPE-SQED中原始指令基于语义等价变换的规则比SQED中原始指令单一复制的规则更灵活，可以提供指令间更丰富的组合，避免了验证自一致性属性下有界模型检测需要展开两倍的深度，从而可以更高效发现大多数长反例轨迹的错误。

SEPE-SQED流程图

SEPE-SQED和SQED的对比结果

全文分享：http://arxiv.org/abs/2404.03172

论文Predicting Lemmas in Generalization of IC3第一作者博士生苏宇恒，通讯作者杨秋松研究员。研究团队通过在IC3算法的归纳泛化中引入预测机制，显著提升了IC3算法的求解性能。

随着电路设计的规模和复杂性不断增大，确保电路设计正确至关重要，形式化技术符号模型检测被工业界广泛采用。但由于电路设计的状态爆炸问题，验证规模仍然有限。IC3算法作为一种基于SAT求解器的符号模型检测算法，相比于其他符号模型检测算法，能够更高效地验证大规模电路设计，在提出后得到学术界广泛关注。

研究团队在IC3算法开销最大的归纳泛化中，根据父引理（parent lemma）和引理传播（lemma propagation）的反例，引入diff set的概念，并计算传播反例和需要泛化的引理的diff set，进而提前预测出一个可能的最小归纳引理。一旦预测成功，将不需要执行后续的泛化过程，从而提高IC3算法的效率。实验结果表明，该方法预测成功率可以达到38.61%，相比改进前的算法，在硬件模型检测竞赛的测试集中多求解出了10个测试用例。

硬件模型检测效果对比

全文分享：https://c56bo58f0a.feishu.cn/file/XE2DbqZhQo7TIAxFCJncqMAYn6d