G中国科学院研究员蔡少伟：S 算法( 三 )

除了形式化验证，在逻辑综合里有很多应用，比如电路结构的优化，找到某个子结构进行替换，在确保替换正确的情况下，要做一些 SAT 去查询两个结构是否可以替换。
在电路测试里，虽然设计过程已经比较准确，但实际上，芯片生产和设计不一定一致，生产过程中存在一些不确定因素，比如杂质的污染导致某条路线、电路路线短路或是断路，会造成芯片与原来设计的不一样。电路测试要做的是尽量覆盖缺陷模型，不会出现类似错误。我们要做的，是产生一组输入向量，覆盖测试的缺陷。
一个常见的缺陷被称为 stuck-at fault，关注路线是不是短路或是断路；此外还有延迟缺陷模型。
如果一条线在我们不知情的情况下断了，得通过测试找出来，只有这条线断了后输出的情况和没断的情况不一样，才能发现异常。一个电路要测试 stuck-at fault，要覆盖两倍电路线数量的缺陷。
比如说，这是三位乘二位的乘法，对应的电路有 50 条线，要检测100 个潜在的stuck-at fault，非常朴素的做法就是把所有可能的输入和实际输出和设计的电路所期待的输出对比是不是一样，不一样就找到一些错误。虽然可以百分之百的覆盖，但太低效，目前产业界不可能做类似枚举。
ATPG 就是利用 SAT 求解器用尽可能少的输入覆盖尽可能多的错误，一般情况下，第一步会随机产生一些输入向量，覆盖大部分要关注的错误，剩下的即是比较难能随机覆盖的，需要通过对应的 SAT 求解器求出可以覆盖对应的 input 向量，最终压缩产生 Bachmark。

文章插图

如图，假设 d 这条线断了，它为 0，要找到一个输入使得正常设计的情况下输出和在另一边输出不一样，从而发现出现断路的情况。
由此，要产生一个满足两个条件的测试向量：一是错误的激活，二是错误要传播，将两个条件编码为一个 CNF 公式，合起来其实也是 SAT 求解问题。
SAT 求解器在 EDA 中如此重要，那么，它目前做得怎么样？
SAT 是一个逻辑问题，很容易会采用逻辑推理的方法思考，比如说归结原理。但把它看作在搜索空间找赋值，判断它是否存在合法的解，因此搜索的方法也可行。
SAT 求解方法可以分为两类：完备算法和不完备算法。完备算法是指算法只要给足时间，肯定会产生正确答案，YesorNo，但这个时间在理论上没有保证；不完备算法是指争取短时间内找到解。
SAT 求解器非常重要，在历史上有很多科学家在研究，完备算法从 1960 年开始有了，不完备算法从 1992 年开始。其中，最重要的是 1996 年 CDCL，它的一个breakthrough。
历史上，1997 年 Bart Selman 提出命题逻辑推理十个挑战，其中第七个是能否结合产生更 powerful 的方法，这是我们近期研究的方向。
以前的方法是侧重于系统搜索和局部搜索，这两个方法求解能力互补，即使采用并集，实际上在工业上没有得到改进，原来的方法不能求解，通过并集的方法也求解不了。
近期，我们基于完备搜索进行求解，把随机搜索的不完备方法当成采样工具，采样的信息帮助完备算法求解，基于信息交互的深度合作。在过去几年比赛的工业实例上，这一方法产生的混合算法可以求解原来两个算法都不能求解的算例，比例达到 12% ，达到了工业实例上的显著改进，首次回答了这一挑战。
同时，这一方法也直接用到实际场景的集成电路验证，可以求解达到近 2 亿子集的1小时求解规模。
在今年的 EDA 比赛，我们拿到全球第二名的好成绩，这说明做好 SAT 求解器对 EDA 十分重要，相关的方法已发表在SAT 2021，获得最佳论文奖。