近日，形式化验证领域著名国际会议Formal Methods in Computer-Aided Design 2024公布了硬件模型检测竞赛HWMCC 2024的结果。中国科学院软件研究所基础软件国家工程研究中心博士生苏宇恒、杨秋松研究员、慈轶为副研究员所研发的硬件模型检测求解器rIC3表现突出，荣获比特级（bit level）赛道和词级位向量（word level bit vectors）赛道两项冠军。

硬件模型检测是指通过算法工具自动化判定该硬件系统是否符合所期望的属性。在电子设计自动化（EDA）软件设计过程中，特别是芯片设计、验证和优化阶段需要广泛使用到硬件模型检测工具。通过自动化和高效的模型检测能帮助工程师发现并修复设计中的潜在问题，从而提升硬件系统的质量及设计效率。

rIC3求解器是基于IC3算法的一款硬件模型检测工具。对于IC3算法所构造的SAT问题，研究团队通过减少每次SAT求解中需要决策的变量数量，同时设计更适合IC3算法的高效数据结构，来提升IC3算法中SAT问题的求解效率。

比特级赛道和词级位向量赛道中的竞赛结果显示，求解器rIC3在一小时内能够比排名第二的求解器分别多求解31个和69个问题。

参赛求解器在比特级赛道和词级位向量赛道的求解效率对比

硬件模型检测竞赛HWMCC已举办12届，此次HWMCC 2024参赛队伍来自斯坦福大学、密歇根大学、清华大学、慕尼黑大学、滑铁卢大学等多所知名高校和科研院所。

HWMCC 2024官网：https://hwmcc.github.io/2024

rIC3求解器工具链接：https://github.com/gipsyh/rIC3