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

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 的输入形式。如果能找到这个公式的解，也就是找到反例，说明是不等价的。反之，如果可以证明这一对应的公式是不可满足的，也就说明这两个电路是等价的，这就是等价性验证目前的技术。