2021年12月9日至11日，第六届全球人工智能大会（GAIR2021）在深圳正式召开。时隔五年，数次翻江倒海，成为迄今为止粤港澳大湾区人工智能领域规模最大、级别最高的跨界盛会。在大会第二天举行的“集成电路高峰论坛：国产高端芯片之路”上，来自学术界、产业界和投资界的15位专家齐聚一堂，共话国产高端芯片实力与RISC-V带。给中国芯片一个机会。EDA是中国芯片产业发展的瓶颈技术，求解器是EDA的基础引擎。只有解决基础技术难题，才能支撑整个行业的快速发展。基于此，中科院软件所研究员蔡绍伟主要从自己的研究角度谈了EDA的发展。蔡绍伟的演讲主要涉及三个方面，一是EDA与SAT求解器的关系；二是说明SAT求解器在EDA中的应用；第三是分享他的团队在SAT求解器方面的进展。蔡绍伟表示，EDA集成电路设计自动化软件整个链条很长，不是单一的软件。在EDA软件中，底层需要一些计算引擎，主要的计算引擎是SAT求解器。SAT求解器用于EDA的各个方面，包括逻辑综合、物理实现以及中间验证和仿真测试。目前，蔡绍伟团队的SAT求解器已经应用于集成电路验证的实际场景，部分规模近2亿条的计算实例可在1小时内求解。以下为蔡绍伟GAIR2021演讲内容，雷锋网（公众号：雷锋网）不改初衷编辑整理：今天的报告分为3个部分：一是EDA与SAT求解器；二是举几个例子说明SAT求解器在EDA中的应用；三是介绍团队在SAT求解器方面的进展。EDA的全称是ElectronicDesignAutomation，是指集成电路的设计自动化软件。有了这样一套自动设计集成电路的软件，EDA一般被称为芯片之母。它是整个半导体的最上游，支撑芯片乃至整个信息产业的共同基础。技术。EDA集成电路设计自动化软件不是一个单一的软件，整个链条很长，我们可以把EDA软件当作硬件编译器，用硬件描述语言写出芯片的需求，通过EDA软件就可以帮我们自动设计芯片集成电路领域。在EDA软件中，底层需要一些计算引擎，主要的计算引擎是SAT求解器。在EDA的各个环节，包括逻辑综合、物理实现、中间验证和仿真测试，实际上都用到了SAT求解器。例如，以逻辑综合为例。在逻辑综合的历史上，SAT求解器一直扮演着非常重要的角色。特别是在逻辑综合发展历史的最后阶段，优化和表示严重依赖于SAT求解器。在电路的形式化验证方面，主要有两种形式化验证工具：模型检查工具和等效性验证工具。模型检验主要用于证明一个电路是否满足某种性质，而等价性验证则用于证明两个电路是否等价。以模型检测技术的发展为例。在这个历史发展阶段，2000年后开始的模型检测技术基本都是基于SAT求解器发展起来的。通常，计算机在解决问题时，有两种思路：一种是用数学语言把问题描述清楚，然后设计算法来解决。这就是约束求解的思路。典型场景包括定理证明。第二个是机器学习。用户提供示例，计算机解决问题。例如，各种模式识别任务更适合机器学习。对于需要严格证明的场景，需要进行约束求解。SAT的全称是Booleansatisfiabilityproblem。这个问题的描述很简单，就是给定一个布尔公式或者命题逻辑公式，也就是用AND或者NOT等逻辑连接词连接的公式，判断这个公式是否可以给定的变量赋值使公式为真。如果存在这样的分配，则称该公式是可满足的，否则它是不可满足的。SAT涉及的基本概念包括变量、词、从句（从句是词的析取）和连词范式（简称CNF，从句的连词，即从句的集合）。SAT的求解一般采用合取范式输入，电路也有SAT问题。关于SAT在EDA中的典型应用，要解决带有SAT的电路中的问题，首先要将电路转换成SAT可以接受的输入形式。其中，有一种比较简单的将电路转成CNF的编码方式，时间线性，标度线性，比较方便。表格左边是电路的逻辑门，右边是对应的SAT公式。这样，电路就可以转化为合取范式，成为SAT的输入形式。刚刚理解的电路可以转化为SAT公式，那么在大多数EDA场景下如何使用SAT求解器呢？举几个例子：首先看模型检查工具。模型检查工具是检查一个电路是否满足某种性质，比如“寄存器肯定不会冲突”。我们需要用自动机模型来表征电路行为，验证的属性用时序逻辑相关的公式来表示。证明这个模型是否可以包含属性，即这个模型下的属性是否为真，这叫做模型检查。此任务的核心需要调用SAT求解器。这是一个计数器的例子，我们拿到硬件描述源Verilog模块，它会从第1位跳到第2、3位，然后重启。编译Verilog模块得到一个网表，包括netgate的寄存器和逻辑门连接，最后得到网表对应的状态转移模型，即自动机模型。有了这个模型之后，还需要得到验证属性对应的公式。有界模型检查是检测K步内是否存在路径（K给定）。前面说了，走完K步后，有没有一条路径违反了规定的性质？这就是为什么我们需要将属性转化为逻辑公式。我们关心两种类型的属性。一个是安全属性，这意味着坏事永远不会发生。用全局顺序词Gp表示，p是要满足的属性。写出公式，先用自然语言理解它。如果存在一条路径，其初始状态可以到达某个状态，而这个状态使p无效，我们就会找到一个反例。如果没有这条路径，则意味着必须在k步内建立Gp。另一个是Liveness属性，表示好事终究会发生，用Fp表示。同样，我们仍然考虑它的反面：如果这个公式不成立，则有一条相应的路径后面跟着一个循环，而在这条路径上的任何状态下p都不为真，所以不满足这个性质。结合以上，可以转化为SAT公式。如果这个公式被SAT求解器判断为可满足的，也就是说它有一个反例，这个反例可以对应构造出来。如果这个公式是不可满足的，也就是说没有反例，这个性质被验证是满足的。第二类形式化验证是等价性验证。两个电路是等效的，也就是说，在任何输入条件下，两个电路的输出都是相同的，它们在功能上是等效的。那么，你如何用SAT做到这一点？首先，可以先考虑单路输出，将N1和N2两个电路的输出通过异或门连接起来。如果能找出一组输入使得异或门的输出为1，则说明N1和N2两个电路的输出不相同，即不等价。如果没有找到这样的输入，则暗示等价。如果有多个输出电路也是如此，将每个对应的输出N1和N2对应的输出异或，最后做一个或门将它们连接起来。使最终门输出为1意味着必须有一对这些输出不相等，因此它们不等价。这个过程可以用SAT求解器来完成，构造混合电路后，就变成了CNF公式，也就是SAT的输入形式。如果你能找到这个公式的解，也就是找到一个反例，就说明它不等价。反之，如果能证明对应的公式不可满足，则说明这两个电路是等价的，这就是目前的等价性验证技术。除了形式验证，在逻辑综合上还有很多应用，比如电路结构的优化，寻找某个子结构进行替换，做一些SAT检查两个结构是否可以替换，如果替换正确的话。在电路测试中，虽然设计过程比较准确，但实际上芯片的制作和设计并不一定相同。由此产生的芯片与原始设计不同。电路测试需要做的就是尽可能的覆盖缺陷模型，这样就不会出现类似的错误。我们要做的是生成一组覆盖测试缺陷的输入向量。一种常见的故障叫做stuck-atfault，主要看路由是短路还是开路；还有一个延迟缺陷模型。如果一条线在我们不知情的情况下断了，我们必须通过测试才能发现。只有断线后的输出与未断线时的情况不同，才能发现异常。要测试电路的固定故障，必须覆盖两倍于电路线路数量的缺陷。例如，这是三位乘以两位，对应的电路有50行。要检测100个潜在的固定故障，非常简单的方法是将所有可能的输入和实际输出与设计电路结合起来。预期的输出比较是否相同？如果不同，找出一些错误。虽然可以100%覆盖，但是效率太低，目前业界不可能做类似的枚举。ATPG是使用SAT求解器以尽可能少的输入覆盖尽可能多的错误。一般来说，第一步会随机生成一些输入向量来覆盖大部分需要关注的错误，剩下的就比较难随机化了。对于覆盖，需要通过相应的SAT求解器得到相应的输入向量，最后压缩生成Bachmark。如图，假设d线断了，就是0，需要找一个输入，让正常设计下的输出和另一边的输出不一样，这样就发现有开路。因此，需要生成满足两个条件的测试向量：一是错误的激活，二是错误必须传播。将这两个条件编码成一个CNF公式，其实就是一道SAT解题题。SAT求解器在EDA中非常重要，那么到目前为止它的表现如何？SAT是一道逻辑题，很容易用逻辑推理的方法来思考，比如解析原理。但是可以把它看作是在搜索空间中寻找一个赋值，判断它是否有合法的解，所以搜索的方法也是可行的。SAT求解方法可分为两类：完全算法和不完全算法。一个完整的算法是指只要给算法足够的时间，它一定会产生正确的答案，YesorNo，但这个时间在理论上是不能保证的；不完整的算法意味着它力求在短时间内找到解决方案。SAT求解器非常重要。许多科学家在历史上一直在研究它。完整的算法从1960年就有了，不完全的算法从1992年就有了，其中最重要的是1996年的CDCL，它的一个突破。历史上，1997年BartSelman提出了命题逻辑推理的十大挑战，其中第七项是能否将它们结合起来产生更强大的方法，这也是我们最近研究的方向。以前的方法侧重于系统搜索和本地搜索。这两种方法具有互补的求解能力。即使采用union，在工业上也没有得到改善。原方法解决不了，union方法也解决不了。最近我们解决了基于完备搜索的问题，利用随机搜索的不完备方法作为采样工具，采样的信息帮助完备算法解决，基于信息交互进行深度合作。在前几年比赛的工业实例中，该方法生成的混合算法可以解决原两种算法无法解决的计算实例，比例达到12%，实现了对工业实例的显着提升，并首次回答了这个挑战。同时，该方法也直接应用于实际场景的集成电路验证，可解决近2亿子集的1小时求解规模。在今年的EDA比赛中，我们获得了世界第二的成绩，可见一个好的SAT求解器对于EDA来说是非常重要的。相关方法已在SAT2021发表并获得最佳论文奖。总结：SAT求解器作为EDA的关键引擎发挥着重要作用。目前这方面的重要进展是混合求解方法的突破。谢谢你们。
