中国科学院研究员蔡少伟：SAT 求解器 EDA 基础引擎 | GAIR 2021

雷峰网(公众号：雷峰网)按：2021 年 12 月 9 日-2021 年 12 月 11 日，2021 第六届全球人工智能大会（GAIR 2021）于深圳正式召开。历经五年，见证数次潮水的转向，成为目前为止粤港澳大湾区人工智能领域规模最大、规格最高的学术、工业和投资领域跨界盛会。

在大会第二天举办的“集成电路高峰论坛：国产高端芯片之路”上，汇聚来自学术界、产业界和投资界的 15 位大咖，共同探讨了国产高端芯片的实力以及 RISC-V 带给中国芯片的机会。

EDA是中国芯片产业发展的卡脖子技术，求解器又是EDA的基础引擎，解决了基础技术挑战才能支撑整个产业的快速发展——基于此，中国科学院软件研究所研究员蔡少伟主要从自己的研究角度谈到了 EDA 的发展。

蔡少伟的演讲主要涵盖三个方面，一是 EDA 和 SAT 求解器的关系；二是举例说明 SAT 求解器在 EDA 当中的应用；三是分享其团队在 SAT 求解器方面的进展。

蔡少伟表示，EDA 集成电路设计自动化软件，整条链很长，而不是单个的软件。在 EDA 软件中，其底层需要一些计算引擎，而主要的计算引擎就是 SAT 求解器。

在 EDA 各个环节中，包括逻辑综合、物理实现，以及中间的验证、仿真测试都会用到 SAT 求解器。

目前，蔡少伟团队的 SAT 求解器已经用于集成电路验证的实际场景，在 1 小时内可求解出一些近 2 亿子句规模的算例。

以下是蔡少伟在GAIR 2021 上的演讲内容，雷峰网进行不改变原意的编辑整理：

今天的汇报分为3个部分：一是 EDA 和 SAT 求解器的关系；二是举几个例子说明 SAT 求解器在 EDA 中的应用；三是介绍团队在 SAT 求解器方面的进展。

EDA 的全称是 Electronic  Design  Automation，是指集成电路的设计自动化软件，用这样一套软件自动设计集成电路，一般都称 EDA 为芯片之母，是整个半导体的最上游、支撑芯片乃至整个信息产业的共性基础技术。

 EDA集成电路设计自动化软件不是单个的软件，整个条链很长，我们可以把 EDA 软件当成硬件编译器，用硬件描述语言写出芯片的需求，通过 EDA 软件可以帮助我们自动的设计出芯片集成电路的版图。

EDA 软件里面，底层需要一些计算引擎，而主要的计算引擎就是 SAT 求解器，在 EDA 的各个环节里，包括逻辑综合、物理实现，以及中间的验证、仿真测试其实都要用到 SAT 求解器。

比如，以逻辑综合为例，在逻辑综合的历史上，SAT 求解器一直扮演非常重要的角色，尤其是在逻辑综合的发展史上最后一个阶段，优化和表示都要极大依赖 SAT 求解器。

在电路的形式化验证方面，形式化验证工具主要有两类：模型检测工具和等价性验证工具。模型检测主要是用来证明一个电路是否满足某个属性，而等价性验证用来证明两个电路是否等价。

以模型检测技术的发展为例，在这个发展历史阶段中，从 2000 年之后开始的模型检测技术基本都是基于 SAT 求解器来开发的。

通常情况下，计算机解决问题的时候有两类思路：一是把问题清楚地用数学语言描述出来，再设计算法求解，这是约束求解的思路，典型场景包括定理证明等。二是机器学习，用户提供例子，计算机解决问题，比如，各种模式识别的任务比较适用于机器学习。对于需要严格证明的场景，则需要约束求解来解决。

SAT 的全称是布尔可满足性问题，这个问题的描述非常简单，即给定一个布尔公式或称为命题逻辑公式，也即用与或非等逻辑连接词连接起来的公式，判断是否能给公式里的变量赋值使得公式为真。如果存在这样的赋值，就说这个公式是可满足的，否则就是不可满足的。

SAT 涉及到的基本概念包括变量、文字、子句（子句是文字的析取）、合取范式（简称CNF，子句的合取，即子句集合）。SAT 的求解一般采用合取范式输入，也有针对电路的 SAT 问题。

关于 SAT 在 EDA 中的典型应用，为了把 SAT 求解电路中的问题，首先得把电路转为 SAT 可以接受的输入形式。其中，将电路转为 CNF 有比较简单的编码方式，有线性时间和线性规模，相对比较方便。

表格左边是电路的逻辑门，右边是对应的 SAT 公式。这样，电路就可以转为合取范式，成为 SAT 的输入形式。

刚刚已经理解的电路可以转为 SAT 公式，那么，如何在多数 EDA 场景中利用 SAT 求解器呢？我们举几个例子：

首先看模型检测工具，模型检测工具是要检测一个电路是否满足某个属性，比如“寄存器肯定不会有冲突”。我们需要用自动机模型把刻划出电路行为，而验证的属性用时序逻辑相关的公式表达。要证明这个模型是否能蕴含属性，也就是在这个模型下的属性是否成立，这个就叫模型检测。这个任务的核心需要调用 SAT 求解器。

这是一个计数器的例子，我们拿到硬件描述源 Verilog 模块，将从第一位跳到 第2、3位，然后再重启。对Verilog 模块进行编译，得到一个网表，包括计存器、网门的逻辑门连接，最后可以得到这个网表对应的状态转移模型，也就是自动机模型。

有了这个模型之后，还要得到验证属性对应的公式。有界模型检测是检测 K 步（K 是给定）之内是否存在一条路径。前面提到，是否存在一条路径走完 K 步后会违反指定属性呢？这就是为什么我们需要把属性翻译成逻辑公式。

我们关心两类属性，一类是 Safety 属性，指坏的事情永远不会发生，是用全局的时序词Gp 表示，p 就是要满足的属性。将公式写出来，用自然语言先理解一下，如果存在一条路径初始状态可以达到某个状态，这个状态使得 p 不成立，我们就找到一个反例。如果不存在这样的路径，说明 Gp 在 k 步之内肯定是成立的。

另一个是 Liveness 属性，是指好的事情终会发生，用 Fp  表示。同样，我们考虑的还是它的反面：假如这个公式不成立，对应有一段路径跟着一个循环，并且这个路径上任何状态下 p 都不成立，因此这个属性就不满足了。

结合前面所说，可以讲将其翻译成一条 SAT 公式，如果这条公式用 SAT 求解器来判定，它是可满足的，就意味着它存在一个反例，并且可以对应地将这条反例构造出来。如果这个公式是不可满足的，就是说不存在反例，这个属性是被验证满足的了。

形式化验证的第二类是等价性验证。两个电路等价，就是说在任何输入的情况下两个电路的输出都一样，在功能上是等价的。那么，这个事情用 SAT 怎么做呢？

首先，可以先考虑单输出的，将两个电路 N1、N2 的输出通过异或门连接，如果能够找到一组输入使得异或门的输出是1，意味着 N1 和 N2 两个电路的输出是不一样的，即不等价。如果找不到这样的输入，则意味着是等价的。

如果有多输出电路也是一样，把每个对应的输出 N1、N2 对应的输出做异或，最后做一个或门连接起来。使得最后的门输出为 1，意味着这些输出肯定有一对是不相等的，所以是不等价。

这个流程可以用 SAT 求解器做出来，构造混合电路后变成 CNF 公式，即 SAT 的输入形式。如果能找到这个公式的解，也就是找到反例，说明是不等价的。反之，如果可以证明这一对应的公式是不可满足的，也就说明这两个电路是等价的，这就是等价性验证目前的技术。

除了形式化验证，在逻辑综合里有很多应用，比如电路结构的优化，找到某个子结构进行替换，在确保替换正确的情况下，要做一些 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 求解方法可以分为两类：完备算法和不完备算法。完备算法是指算法只要给足时间，肯定会产生正确答案，Yes  or  No，但这个时间在理论上没有保证；不完备算法是指争取短时间内找到解。

SAT 求解器非常重要，在历史上有很多科学家在研究，完备算法从 1960 年开始有了，不完备算法从 1992 年开始。其中，最重要的是 1996 年 CDCL，它的一个break  through。

历史上，1997 年 Bart Selman 提出命题逻辑推理十个挑战，其中第七个是能否结合产生更 powerful 的方法，这是我们近期研究的方向。

以前的方法是侧重于系统搜索和局部搜索，这两个方法求解能力互补，即使采用并集，实际上在工业上没有得到改进，原来的方法不能求解，通过并集的方法也求解不了。

近期，我们基于完备搜索进行求解，把随机搜索的不完备方法当成采样工具，采样的信息帮助完备算法求解，基于信息交互的深度合作。在过去几年比赛的工业实例上，这一方法产生的混合算法可以求解原来两个算法都不能求解的算例，比例达到 12% ，达到了工业实例上的显著改进，首次回答了这一挑战。

同时，这一方法也直接用到实际场景的集成电路验证，可以求解达到近 2 亿子集的1小时求解规模。

在今年的 EDA 比赛，我们拿到全球第二名的好成绩，这说明做好 SAT 求解器对 EDA 十分重要，相关的方法已发表在SAT 2021，获得最佳论文奖。

总结：SAT 求解器作为 EDA 关键引擎起到重要的作用，这方面的重要进展目前是混合求解的方法取得突破。谢谢大家。