算术电路

算术电路是计算机硬件中必不可少的电路，它的性能是决定计算机能力的重要因素。计算机中采用的是二进制系统，它为了能表示正、负数，必须将数冠以符号位，同时为了能用同一硬件实现加、减运算，常采用补码运算，为此增加了判别符号及码间转换等辅助电路。

结合半加图的算术电路等价性验证技术为了克服现有等价性验证技术难以快速验证复杂算术电路的局限性，提出了一种利用综合引擎分析并再现算术电路优化过程的算法。该算法结合了乘法器的编码方式识别技术、加法电路的半加树提取技术和部分积加法电路的架构识别技术来提取乘法电路的实现结构，以此生成与实现电路结构相似且逻辑正确的网表。针对算术电路结构的相似性，仅分析低位输出的电路架构以降低算法复杂度。实验结果表明，与传统的算术电路验证算法相比，该算法可以明显提高算术电路的验证速度，并且可以直接结合到现有的寄存器传输级(RTL)和门级网表的验证流程中，从而提高了算术电路的验证能力。1

电路实现方案提取算法算术电路架构识别算法中m、n为循环次数，m为启发值。首先构建电路的AIG，其次选择输出out，提取所对应的HAG，根据HAG拓扑结构确定电路的实现方案Πi，记录Πi出现次数，返回出现次数最多的Πi。乘法电路中的编码逻辑会引入‘’异或‘’运算，这部分逻辑会干扰HAG的提取，因此应该对这部分逻辑进行预处理。1

HAG提取算法提取HAG是以AIG为基础，构建AIG的伪代码如下。

Algorithm create vetex(p1，p2){Special case preprocess；If Hash lookup(p1，p2)does not find vertex p {Create vertex p；Add p to Hash table;} Returnp；}

其中，p1、p2 是待新建节点的2个输入节点，在构建节点p之前，首先对特殊情况进行预处理，如判断p1、p2是否为常数节点或是否互相等价等；然后进行哈希查找，判别待构建节点是否已经存在，如果存在则直接合并同构节点，反之则新建节点p；每个新建节点都将加入到一个哈希表中，此哈希表使用节点p的输入p1、p2属性作为关键字。

提取原始电路中的‘’异或‘’(XOR)关系。由AIG容易提取出大部分‘’异或‘’关系。因为A∧B =!(A∧～B)，所以还需要提取‘’异或非‘’(XNOR)关系。在提取出大部分‘’异或‘’(或‘’异或非‘’)运算后，剩余的少量‘’异或‘’关系可以由可满足性问题(satisfiabilityproblem，SAT)引擎和二值决策图(binary decisiondiagram，BDD)引擎辅助得到。

根据已得‘’异或‘’关系寻找输入对应的进位逻辑，添加半加器或全加器，同时需要注意由于常数输入而引起的全加器退化。例如，对于全加器的实现逻辑为

sum=a∧b∧cin，cout=a&b+b &cin+cin &a，当cin=1时，其实现逻辑将退化为sum=～(a∧b)，cout=a+b。

在AIG上标记已经匹配的节点，由已得HAG继续增量式地匹配未被匹配区域直至完成。若遇到加法部分的局部优化引起无法直接匹配加法器，则回溯电路，找出它对应的I集合，然后找出该集合对应的‘’和‘’节点，根据推论变化对应的HAG的结构，对电路进行局部扩展，直至其对应的输出可以与未匹配的部分电路匹配。1

结合HAG的算术电路验证算术电路是等价性验证领域的瓶颈，商业工具为单独验证算术模块提供了黑匣子技术，用户可以设置算术电路的实现方案。当用户不了解算术模块的实现方案时，在黑匣子技术基础上，算法可以直接结合到现有的RTL和门级网表的验证流程。该流程不仅对乘法电路有效，对于其他以加法为基本实现单元的算术电路，只须进行HAG架构的提取，即可得到实现架构的相关信息。

在读入的实现电路中选择低5、6位的输出作为起点，回溯电路构建AIG，同时标记各 节点对应的输出编号，分组节点。分析高位输出对应的输入集合，根据电路性质确定电路的编码方式。由输出回溯电路，在AIG上提取‘’异或‘’关系，对乘法电路进行预处理，匹配半加器建立HAG，继而识别原始操作数的性质，得到HAG架构。根据得到的编码方式和HAG架构综合参考电路，获得与实现电路结构相似的参考电路网表。当提取编码方式和HAG架构时，估算m×n(m>n)的并行乘法器的算法复杂度：乘法器涉及的加法器数目为О(m ×n)，m ×n个部分积的位。搜索的输出为5、6位，涉及的加法器个数为常数，并且这样的搜索是一次性的，因此该复杂度在实际的电路设计中可以忽略。根据这些特征信息，综合引擎可以生成与实现电路结构相似的网表，从而提高等价性验证的效率。1

算术电路的等价性验证提出了一种利用综合引擎重现算术电路的优化过程的算法，提高了等价性验证效率。ZDVF的综合引擎首先识别乘法器的编码方式，提取部分积的加法树实现方案；然后根据这些信息生成与实现电路结构相似且逻辑正确的网表。算法可直接结合到现有的RTL和门级网表的验证流程中，从而提高算术电路的验证能力。2

加法树构架提取乘法器的加法树输出在组织结构上具有相似性，因此只需针对部分低位输出提取加法树。由半加器的位置和操作数的性质即可识别加法树的构架。

wallance tree结构的加法树可由CSA(斜进位加法器，carry一save adder)实现，最后 一次输出终值的加法采用了带进位链的高速加法器。远离输出的CSA的操作数大多为部分积，而靠近输出部分的CSA的操作数都基本是前级加法器的进位与和位。在阵列乘法器中其全加器的操作数除最后一次终值输出之外，操作数都包括了I，S和C。从而可区分出乘法器的不同加法构架。实验中，提取了低六位输出的加法树就可区分出不同的加法树构架。2

验证框架算术电路是等价性验证领域的瓶颈，商业工具为单独验证算术模块提供了黑匣子(blackbox)技术，用户通过其可设置算术电路的实现方案。当用户对算术模块的实现方案不了解时，算法可在黑匣子技术基础上，直接结合到现有的TRL和门级网表的验证流程中。在提取编码方式和加法树构架时，估算m*n(>mn)的并行乘法器的算法复杂度：乘法器涉及到的加法器的数目为0(mn)，mn个部分积的位。搜索的输出为3～6位，涉及到的加法器个数为常数，并且这样的搜索是一 次性的，因此该复杂度在实际的电路设计中可忽略。根据这些特征信息，综合引擎可生成与实现电路结构相似的网表，从而提高等价性验证的效率。2

实验结果算法在ZDFV的逻辑综合引擎上实现，分析实现电路，提取特征信息并生成与实现电路的具有相同实现方案的网表。测试平台是Snu的Ultra一Sparc60工作站，其配置为双CPU，ZG内存。乘法器的实现有CSA阵列乘法器，Wallace tree乘法器。

提取电路特征时间，消耗集中于加法图的提取，但该时间并不正比于电路规模。FORMALITY的验证时间，实现电路是以对应实现方案实现的乘法电路，参考电路分别是阵列结构乘法器和引擎相应实现的综合结果。当乘法器的位数达到14位时的网表文件，FoRMALITY运行时间过长，所以给出的电路规模只到12位。算法还实验了各种类型的表达式和乘法结构，有符号的、无符号的及布什算法，结果类似。2

本词条内容贡献者为:

刘宝成 - 副教授 - 内蒙古民族大学