球友会qy

近期，中国科研实验室软件研究所在形式化验证领域的模型检测方面取得系列进展，2篇成果论文被国际计算机辅助验证会议CAV 2025接收，其中工具长文The rIC3 Hardware Model Checker获杰出论文奖。还有1篇被计算机设计自动化会议DAC 2025接收。

CAV 2025杰出论文奖证书

以下是相应成果介绍，欢迎探讨研讨。

The rIC3 Hardware Model Checker

作者：苏宇恒，杨秋松，慈轶为，卜天峻，黄子彧

录用会议：CAV 2025

内容简介

在集成电路设计复杂度不断提升的背景下，形式化验证技术的重要性日益凸显。IC3算法作为一种基于SAT求解的符号模型检测方法，因其完备性和良好的可扩展性，已成为主流模型检测工具的核心组件，并在工业验证中得到实际应用。

为提升IC3算法的求解问题规模和求解效率，研究团队结合多项前沿优化技术，基于Rust语言研发了硬件形式化验证工具rIC3。该工具采用深度优化的SAT求解器、扩展的CTG泛化方法、以及动态调整的泛化策略等多项技术，有效提升了求解性能。

rIC3具有出色的求解性能和对于求解问题的可拓展性。在2024国际硬件模型检测竞赛中，rIC3分别取得了比特级和词级位向量两个赛道的第一名，与其他开源工具（如ABC和nuXmv）相比表现出显著优势。现在，rIC3已接入开源EDA软件SymbiYosys的后端，可用于RTL验证，并给予证明或反例。

求解效率对比

论文链接：http://doi.org/10.48550/arXiv.2502.13605

工具代码链接：http://github.com/gipsyh/rIC3

Deeply Optimizing the SAT Solver for the IC3 Algorithm

作者：苏宇恒，杨秋松，慈轶为，李蓥成，卜天峻，黄子彧

录用会议：CAV 2025

内容简介

面对系统变量数量增加导致的状态空间指数级膨胀，IC3算法在处理大规模设计时仍存在挑战。为提升IC3算法的性能和可扩展性，研究团队分析发现，IC3算法生成的SAT问题单次求解时间短（通常在毫秒级），但需要处理的问题数量庞大。基于此，研究团队采用Rust语言实现了一个轻量级SAT求解器GipSAT。

该求解器在每次求解前将进行变量相关性分析，把后续变量决策和布尔约束传播的变量赋值限制为决策的变量子集，减少处理无关决策变量；针对求解简单问题的特点，将决策启发式的优先队列替换为更高效的桶结构；引入了支持临时子句的机制，避免频繁重置求解器。

实验数据显示，GipSAT相比轻量求解器Minisat平均取得3.61倍的性能提升。相比CaDiCaL和CryptoMinisat，GipSAT平均性能提升5.99倍和4.83倍，而且在相同时间内能够处理更大规模的问题，为提升IC3算法的实际应用能力给予了有效解决方案。

实验结果对比

论文链接：http://doi.org/10.48550/arXiv.2501.18612

Leveraging Critical Proof Obligations for Efficient IC3 Verification

作者：朱凌峰，张昕荻，李勇坚，蔡少伟

录用会议：DAC 2025

内容简介

IC3算法的运行是顺利获得逐步构建归纳不变式，证明系统安全性或发现违反规约的反例。在此过程中，证明义务（Proof Obligation，PO）作为IC3算法的核心机制，用于追踪当前需要阻断的不良状态。然而，现有IC3算法对所有PO采用统一处理策略，未能区分不同PO对引理传播与帧精化的贡献差异，导致计算效率受限。

针对这一问题，研究团队提出了“关键证明义务”（Critical Proof Obligation，CPO）的概念，将直接影响引理传播的PO识别为CPO。基于此，团队设计了两项优化策略。一是在SAT求解过程中，根据历史CPO的出现频率调整假设文字的优先级，使求解器更倾向于生成包含关键变元UNSAT核，从而提升引理泛化的有效性；二是只有当与引理相关的所有CPO被阻断，相关引理才能被有效向深层帧传播，以避免冗余引理积累。

研究团队将上述优化策略集成至开源求解器IC3ref和自研工具Modelchecker，分别以-uc与-pr参数开启优化功能，并顺利获得HWMCC 2019至2024的公开基准集（共786个测试用例）进行评估。实验结果显示，团队优化版本在IC3ref额外解决了18个问题，性能超过ABC、IC3ref-CAV23、IC3ref-DAC24三款工业界先进IC3工具。在Modelchecker中，优化版本在验证时间与求解能力上均有提升，展现了方法的通用性。此外，团队还顺利获得引入CPO识别率与引理传播成功率两项评价指标，量化验证了优化策略的有效性。

实验结果对比

团队基于Modelchecker构建了香山缓存（TileLink版本）的自动化验证流程，实现从Chisel硬件设计到反例波形图的全链路验证——将Chisel代码转换为Verilog→顺利获得Yosys工具生成AIG电路模型→调用Modelchecker进行形式化验证→若发现错误则自动生成反例波形图辅助调试。团队顺利获得该验证过程，完成了对L3缓存性能瓶颈分析，验证时间较商业工具JasperGold缩短35%；顺利获得比特级建模发现潜在死锁问题，为香山缓存的缺陷定位给予了形式化依据。

论文代码：http://github.com/ISCAS-modelchecker/modelchecker

约束求解研究室网址：http://solver.ios.ac.cn/