【本文暂时只适合快速阅览，slides待上传】

这篇文章是一篇我在 Raina Technology 的报告演讲稿，所有基于的内容都是开源的。文章内部本身没有任何引用的图片，需要结合slides的内容进行阅读。 内容关键词集中在EDA、ABC、AIG、组合逻辑、时序逻辑、等价性验证等。 新手友好，内容没有过多的深入，老少皆宜。

大家好，欢迎来到知识分享系列，本次主要围绕AIG，主要从问题、概念、ABC中的AIG处理和ABC中的等价性检查四个方面给大家讲解。 这样安排的主要原因是，当我们把一个知识领域封装成一个完整的问题的时候，我们面对的就是任务驱动型学习方式，通过任务驱动的方式，我们能够更加精确地找准要对接的方向，缩小学习压力以提升学习效率，这也是如何在短时间内准备一个局部领域知识的方法。 以下要讲的内容我会以通俗易懂的方式描述出来，即便没有一点基础，也能够轻松驾驭，前后耦合关系比较强，大家有什么问题可以记下来，在结束之后一并提问。

首先说一下，我们这次知识分享的知识在EDA全流程中的位置。

基于之前洋哥给大家的EDA培训，我们知道有两个很重要的部分一个是Synthesis，另一个是Verification，现阶段以青松等同事帮助我们搭建的Openroad的流程框架之中有个模块叫yosys，yosys集成了很多工具，那么其中就包括ABC，ABC是我近期研究的对象，那么ABC也正是一个支持时序逻辑的Synthesis和Verification的工具，这里我们没有用工具集而用的工具来描述是因为ABC有很多的功能但是非常完整，单一的拆分比较的复杂，也是未来Berkeley小组的研究对象（future work），根据洋哥推荐的西电国微系列视频我们也知道EPFL也在解耦相关领域也做了工作。

首先是问题，抛出一个问题：

如何对两个AIG做等价性检查？

我们看到这个问题的时候首先想到的是什么是AIG？什么是等价性检查？

由于问题具有跳跃性，我们首先了解其他几种表示布尔函数的方式，由于我们今天的分享同时也涉及布尔表达，真值表是我们最常见的了，问题中出现的AIG也是一种布尔函数的表达形式，我们先来看一种在历史长河中活跃了很久的表达形式：BDD。 BDD是Binary Decision Diagram的缩写，直观上看从根节点到子节点实际上就是真值表的直观表示，它的表示不关心函数内部操作符的表示，仅展示出输入和输出之间的关系；实际上从根节点往下一层一层看，就是香农展开。 香农展开的变量所对应的子式被称作positive cofactor和negative cofactor，cofactor、factor、refactor在我们的语言环境中指代的是完全不同的东西，我们需要区分并理解。 factor的定义跟flatten、substitution等定义是平级的，它代表将表达式化简到literal到数量最少，这种表达形式甚至可以做物理消耗上的估算。refactor我们下面会提到。

这里插一句，我们能看到slide此处展示的BDD表示的实际上是一个majority函数，majority函数是一个非常有趣的函数，在我的ABC分享资料中对它也有些证明和讲解，它以“多于半数决定策略”的特性使得在化简上拥有很大的灵活性，而且在量子计算中inverter，也就是我们说的反相器的实现成本也比majority器件高很多，majority的应用前景值得我们期待，感兴趣的同学也可以自行查阅相关资料。

大多数当下文献中提到的BDD实际上指的是ROBDD，因为由于多年的发展，ROBDD已成为主流，ROBDD是Reduced Ordered BDD，也就是说化简了、有序了的BDD，那么它相对于BDD有什么优势呢？ROBDD的优势在于它对于每一个布尔函数，是唯一的，你找不到任何其他结构能够表示出相同的函数。它的唯一性使得当你得到ROBDD之后，比较两个ROBDD是否相等时常数时间复杂度的。

我们看到这里有张图，描述了ROBDD之间的一些操作，我们称为operation，简单来说就是布尔函数和布尔函数之间的运算，这里展示的是BDDAPPLY操作，就是两个函数的或操作，实际上就是节点跟节点之间的运算。感兴趣的同学之后可以自己手写一下，感受下它的运算过程。如果你真动手写了的话，会发现实际上我们会遇到重复计算的点，比如图中所示的$a_3,b_3$我们计算了两次，那么对于我们直观来讲就是一个优化点，稍微有点算法基础的同学都应该知道如果我们后续有潜在的可能还会用到我们之前计算过的值的话，我们第一个联想到的就是用哈希表来存储我们计算过的值。ROBDD在后续的研究和优化中也确实这样做了，当然还有很多其他的优化方式，比如complemented edge（互补边）等等，感兴趣的同学可以拓展开来，此处不做赘述。

说完BDD，我们再来看看AIG。

什么是AIG，他又是什么样的表达形式呢？ AIG，是And-Inverter Graph的缩写，见名知意，是与逻辑和反转逻辑表达的函数，为什么能这样表示呢，因为与和非在离散数学上能够完全表达一个函数。右边有两个对于一个函数表达的例子，我们能够看出对于一个相同的函数，实际上AIG有不同的表达形式，可能有同学会根据BDD到ROBDD的过程想到结构哈希的方法来调整AIG的结构，结构哈希简单讲就是使得AIG中没有冗余或者相同的节点，但实际上结构哈希的方式也不能够使得两个AIG完全相同，比如以左图为例，$f=abc$，这两个AIG图都将该函数表达成了最简形式，但是两个AIG的表达却不一样。

现在简单说明下为什么我们要选择AIG，有以下三个方面，第一个是便于结构哈希，第二个是可以添加互补边（但实际上BDD中也可以集成这个特性），第三个是具有规律性，这里的规律性是指由于仅仅存在与逻辑和反转逻辑，输入输出在定义上比较规范，极大地减少了“内存足迹”（memory footprint）。

在其他领域里还有MIG，XAG等。

下面我们简单介绍ABC，我们知道之前听到很多的yosys这个synthesis工具中集成了ABC，ABC本身自己是什么呢？ABC是Berkeley自己开发的一套支持时序逻辑的开源综合和验证工具，一直在实时更新，它主要应用的数据结构就是AIG，当然也保留了一些例如netlist、logic Network的支持，但都是为了迎合老的工具比如SIS、VIS和MVSIS。其中MVSIS的开发手段被广泛拓展应用到了ABC中。ABC对这些逻辑优化算法都是实验性的，大家如果看的话也要保持着学习、参考、质疑的态度。ABC他自己是一个工具的集成体，由于多年的开发，耦合性极强，很难解耦，所以Berkeley自己的小组也将“做出分离的单一工具”作为他们未来的目标。这样以来，用户对于工具集的可玩性增加，自定义的范围增大，而非单一的一个巨大的完整工具。

等价性检查在我们现在的语义环境中主要分为两个方面，基于组合逻辑的等价性验证和基于时序逻辑的等价性验证。 组合逻辑会比较直白，核心就是关于布尔逻辑函数的化简并基于BDD（ROBDD）进行结构上的等价性验证或者添加异或逻辑之后基于SAT-solver做可满足性检查，如果有可满足的解，就表明两者不等价。 关于时序逻辑的等价性检查会比较复杂，涉及状态的转换，会转换成有限状态机（FSM），这里不做过多的赘述。

现在我们正式走进ABC中的AIG。

像我们之前所说，ABC主要使用的是AIG作为中间表达方式，逻辑上是与非逻辑，在实际的表示和操作过程中，AIGER被引入ABC，在ABC当中的格式主要有两种，一种是ASCII形式，后缀为.aag，另一种是二进制形式，后缀为.aig，两者之间可以互相转换，ASCII形式的对于用户来说更加具有可读性。aag中偶数的输入代表的是正输入，奇数代表对偶数的输入取了非。感兴趣的朋友可以手动在纸上画一下感受一下aag的表达。

目的跟传统工具一样，就是要对AIG做优化，比如去除冗余节点，找到更好的逻辑边界，快速获取共享逻辑，简化表达等等。 我们将选取三个命令对AIG的优化进行阐述，AIG的优化远不止这些命令，感兴趣的同事可以自行查阅ABC的官网浏览一些主要的命令集合，当然了，即便是ABC的官方网站命令的种类也不完善，需要大家自行在代码中help出所有的命令查看用法。

Rewirte的灵感来源于Formal Verification的一篇文章，在原文中就如同展示中所示，只关心的是二层的子图的优化，并且只注重压缩没有注重层级的增加带来的潜在时延的风险。 Rewrite只注重一个节点的4-feasible cut，遍历的过程是根据拓扑排序推进的。关于 k-feasible cut 的概念，大家同样可以参考技术文档，有详细的描述。总体来讲，原理上就是计算每一个4-feasible cut的布尔函数，NPN-equivilance class可以通过一个表的查找来进行，在这里面找到一个能带来最大性能提升的替换等价图，将原图进行替换。就4个输入的变量来说，有222个equivalence class，在研究中仅100来个出现在了业界的benchmark中，只有将近40个会带来性能上的提升，这40个左右的子图已经被预计算并保存在了一个将近2000个拥有共享节点的AIG中，供ABC使用。 除了这一点，AIG的rewrite同时要注意时延的重要性，由于单纯的对于子图的局部替换有可能在面积减小的同时，critical path的长度会增加，导致层级的个数增加，最终导致时间延迟的增加，所以，delay-aware在rewrite的过程中同样重要。这里如果大家看过Sherry之前在飞书中分享的VLSI的课程的话就会了解一个叫做slack的概念，在这里slack的概念在广义上是相同的，都可以想象成一根皮筋的松紧程度，如果子图的改写优化没有超过slack的容量的话，都是可以进行的，但是超过slack的容量会导致critical path的增加是我们不愿意看到的，如果有同学想了解更多关于slack的相关概念，也请参考技术文档。

Refactor能够处理比较大的cut，通常 K-feasible 中的K能够达到10到20之间，将其转换成BDD同时转换成SOP，再factor，后来用基础的AIG rewrite方法再生成新的AIG子图，当然了，并非所有的结果都会被纳入替换使用行列，当且仅当节点层级和叶子没有增长。 在将BDD转换成SOP的过程中使用了 Minato-Morreale Algrithm ，这个算法的特性是在固定的变量排序下生成唯一的无冗余的SOP表达式并适合做factor操作。（实际上用ESPRESSO算法或者SIS中的simplify命令也可以实现生成无冗余的SOP表达式，但是由于不能够在给单一变量赋值的情况下化简成单纯包含其他变量的表达式或者0，1，即无法做简单无交集化简。）

AIG中对节点的Balance的核心思想很简洁，在每一个节点应用 $a(bc)=(ab)c=(ac)b$ 以最大限度地削减AIG的层级，通常情况下AIG的层级会得减少。

那么从上述的描述我们可以总结出 Rewrite/Refactor 在不增加延迟的情况下削减面积，Balance 是在不增加面积的情况下削减延迟。

为了保证每一次的化简优化过后的结果和原先的结果是等价的。及时发现错误。

在组合逻辑的等价性检查的过程中，最常用的两种方式就是使用BDD和SAT-solver，现阶段研究中常用的还是SAT-solver，相比较于BDD（我们此处说BDD就指代ROBDD），研究表明SAT-solver能够处理更加庞大的业界的benchmark，也有更好的表现，BDD通常表现出的在设计较大时会导致不可接受的时间消耗。而且此处还要注意，虽然我们此处BDD指代ROBDD但是从BDD到ROBDD的过程中order的选择十分重要，实际上不同的order表达出的图的大小也完全不一样，找到最好的order使得ROBDD最小化是一个coNP-complete问题。 BDD和SAT-solver的另一大区别就是Boolean Constraint Propagation的问题，在优化的过程中会有很多的cut，BDD在数据结构上如果有多余的变量要加入需要重新加入表达式构建，但是SAT-solver却能够处理信息的传递。

在ABC中，默认的cec中的SAT-solver是Mini-SAT，它获过多次比赛奖项，轻量级，代码精简，感兴趣的同学可以参考技术文档的该部分。 当然了，传统的Mini-SAT实际上并不能够被直接用在等价性检查中，因为它依旧会比较慢，主要的原因是来自于他紧凑的数据结构，和过高的内存消耗，对于数据结构的转换需要AIG到CNF再做SAT-solver的验证。 同时出现的比较出名的还有PDR，PDR本身并不是好开发者给出的名字，开发者在实现IC3的时候所应用的方法之后被Berkeley的实验室命名为了RDR，感兴趣的同学同样，请前往技术文档，IC3本身是有点复杂的，涉及到一些inductive invariant的概念，有些晦涩难懂，本身我自己也还在学习中，希望大家多多交流。

我们知道在ABC当中miter既代表一个合并两个组合逻辑AIG的命令，在数据结构上又代表一个大的AIG，在做等价性检查的过程当中，由于业界电路规模的不断扩大，直接读入AIG对于SAT-solver来说也成为了比较重的负担，在做等价性检查的过程当中，如何拆解miter成为了研究的主题。在ABC当中，cec对于这种情况处理的机制是首先做SAT-sweeping，简单来讲就是找到一些miter中的共享逻辑，这些共享逻辑可以直接降低后续SAT-solver的调用次数，使得等价性检查的时间得到优化，在ABC当中他还有一个别称的命令是 fraig ，也就是我们所说的function reduction aig。在这之后还需要做的就是logic simulation，logic simulation的主要操作方式就是随基地选取输入的vector，对AIG进行简单的测试，找到一些潜在的等价点和一些一定不等价的点，这种试错的方式能极大地提升验证的效率。这些潜在的等价点（potential points）将会被放在一个class当中，并生成一个暂时的小的miter，这些小的miter由于互相之间互相不影响，等价性的检查相对独立，所以可以将这些小的miter做并行化运算。在Berkeley小组的论文中提及（在slides当中做了引用，感兴趣的同事可以参考）了该实验的结果，在实验所用的业界的benchmark上，等价性验证的时间由超过24个小时压缩到19分钟，性能有了极大的提升。

本期主要的内容是关于ABC中的AIG以及一些等价性检查的问题，知识分享到此结束，请大家阅读相关的技术文档，有任何问题请在飞书上跟我交流。 谢谢大家。