Revisiting Assumptions Ordering in CAR-Based Model Checking

Yibo Dong

doi:10.1109/TCAD.2025.3551658

Revisiting Assumptions Ordering in CAR-Based Model Checking

0

PRE

AI

DOI：10.1109/TCAD.2025.3551658

原文链接

原文求助

摘要

En 中文

模型检验是一种广泛用于硬件验证的自动化形式化验证技术。当前基于IC3/PDR及其通用变体CAR的最先进完整模型检验技术，基于通过多次调用SAT求解器来计算符号化的欠近似和过近似状态集（称为“帧”）。这些技术的性能对SAT求解器被调用时的假设顺序敏感，因为它会影响求解器在公式不可满足时发出的不可满足核——这些核在公式不可满足时由求解器发出，并关键性地影响搜索过程。这一观察结果先前已被发表（Dureja et al., 2020），其中提出了两种部分假设排序策略，即交集和旋转（部分指的是它们仅确定一部分文字的顺序）。在本文中，我们基于对其有效原因的分析，扩展并改进了这些策略。我们证明交集之所以有效，是因为我们称之为核的局部性，而我们的改进策略基于这一观察。我们以对各种排序技术的广泛实证评估结束本文。我们的一种策略，Hybrid-CAR，它能在运行时切换策略，不仅优于其他固定排序策略，还优于其他最先进的错误查找算法，如ABC-BMC。

Keyword:

Complementary approximate reachability (CAR)

hardware verification

model checking

Revisiting Assumptions Ordering in CAR-Based Model Checking

摘要

期刊

机构

引用论文