2.3 逻辑优化核心：AIG 与布尔重构

2.3 逻辑优化核心：AIG 与布尔重构

本节摘要：现代综合引擎的优化主体是 AIG（与-非图）上的布尔重构：以 rewriting（局部窗口替换）、refactoring（大锥重综合）、resubstitution（借已有信号表达新信号）为核心手段，用结构哈希与 SAT 扫描保证进程不膨胀、结果不越界。本节逐个拆解这些算法的机制与复杂度，并解释为什么"大胆变换 + 等价校验"能同时拿到优化收益与正确性保证。SVG 图将展示重构前后 AIG 的结构变化。

为什么优化算法都长在 AIG 上

2.1 节留了一个伏笔：布尔网络是综合的工作表示，而 AIG 是它的极限简化。每个节点只有一种类型（二输入与门），取反挂在边上。这个简化带来的工程收益在重构算法里全面兑现：结构哈希把每个与门节点按两个孩子的编号加取反标志做键，存入全局哈希表，重复子电路自动合并成同一个节点指针；任何以节点指针为键的缓存（如 SAT 结果缓存、优化收益缓存）天然一致；一个网表百万节点也只是百万个定长记录，内存与遍历成本都可预测。UC Berkeley 的 ABC 工具是这套思想的集大成者，学术基准与工业原型引擎大量构建在它之上。

AIG 的规模指标是节点数与层数（关键路径上的门数），分别近似对应面积与时延。重构算法的目标函数因此很简单：在保持外部功能不变的前提下压节点数或压层数。难就难在"保持功能不变"——精确判定两个布尔函数等价是 NP 难问题，工程解法是双保险：优先做保结构的变换（天然等价），以及用 SAT 等价扫描（SAT sweeping）事后清理被证明等价的冗余节点。

rewriting：局部窗口里的模式替换

rewriting 的思路来自编译优化的树模式匹配：以每个节点为根，截取一个最多 4 个输入的小锥（cut），枚举这个小锥功能的所有 4 输入 AIG 实现（预先算好约 220 万种结构存成表），选择其中节点数或层数最优的那个替换。因为替换的是功能等价的小锥，正确性无需验证。单次替换只动几个节点，成本近乎常数；对全图百万节点扫一遍的总代价线性偏常数。它的局限同样明显：窗口太小，看不到跨节点的全局重复——这正是一遍 rewriting 通常只拿到一到两成收益、需要与更大手段组合的原因。

rewriting 单步示意（目标：减少节点）

替换前（7 节点小锥）          替换后（5 节点等价锥）
    o                             o
   / \                           / \
  o   o                         o   o
 /|   |\                        |   |
o |   | o                       a   b
| |   | |                        \  /
a b   c d                        e=o 与 b
（存在重复子式）                 （变量 e 提取后共享）
​

refactoring 与 resubstitution：看得更远的两只手

refactoring 把窗口放大到整个输出锥（可含几十上百节点）：取出一个输出所依赖的最大锥，用真值表或 SOP 形式重新综合（因式分解、代数重写），若新实现更省就整体替换。窗口大，收益潜力大，但大锥的真值表有 2 的 k 次方行（k 为支撑变量数），k 超过 16 代价陡增，所以 refactoring 通常只对局部支撑小的节点做。它专治 rewriting 看不见的病：一片逻辑被十几处重复实现时，逐节点 rewriting 各自局部最优、谁也合并不了谁，refactoring 一次重综合就能把公共因子全部提出来。

resubstitution 的想法更巧：不重算，借力。目标节点 f 的新实现允许引用图里已存在的其他信号（不一定在 f 的原有支撑集里）。若存在关系"f = g 时候保持一致"（即 f 与 g 只在少数输入模式下不同，差异可由一两个已有信号修正），就能用 g 加少量逻辑替掉整个 f 锥。一个具体场景：第 37 号节点恰好与第 5 号节点在 32 种输入组合里只差 2 种，而那 2 种可由已存在的信号 s 区分——于是 37 号节点整个锥被一次"引用 + 修正门"替代，几十个节点消失。发现这种关系靠的是 SAT 求解器：把"存在使 f 异于修正式的输入"编码成可满足性问题，UNSAT 即证明替换合法。

SAT sweeping：等价清理的例行公事

重构一轮后，图里往往积累了大量功能等价但结构不同的节点对。SAT sweeping 的流程是：先用轻量的仿真（随机向量加结构签名）把候选等价对分桶，再对每对候选调用 SAT 证明等价或找出反例，证明等价的节点合并。合并会让图持续收缩，后续重构在更小的图上跑，形成正反馈。等价合并还顺带服务一个更重要的客户——第 6 章的等价性检查：综合引擎保存重构前后的映射点，验证工具只需在映射点间做增量等价证明，避免对整图从零证明。

图：AIG 布尔重构的完整工作环

工艺映射：从抽象门到真实单元

重构完成后的 AIG 仍是抽象电路，最后一步工艺映射（technology mapping）把它翻译成工艺库里的真实单元（标准单元库中的与门、或门、多路选择器、触发器）。主流方法 cut-based mapping：为每个节点枚举与库单元输入数匹配的 cut，动态规划求覆盖全图的最优 cut 选择，目标是最小化面积或时延。映射结果绑定到具体单元后，2.4 节的数值优化与第 3 章的物理实现才有了明确的操作对象。至此，"RTL 进、门级网表出"的完整综合闭环走通，等价性检查（综合器内建 + 独立签核工具复核）为这条链背书。

用一组公开基准的量级感受一下效果：EPFL 等公开算例集上，一轮"重构加扫描"的组合拳通常能把加法器与控制逻辑混合网表的节点数压掉一到两成、层数压掉一到两成，五到八轮迭代后收益递减收敛。工业综合器在这个内核外面再包上时序驱动加权、工艺约束与物理感知信息，形成完整产品——但拆开看，核心就是本节这四件套。

本节要点回顾

• AIG 的工程红利：单一节点类型让哈希、缓存、遍历全部简化，是重构算法的公共底座。
• rewriting：四输入小锥查表替换，保结构等价、单步近常数代价，收益一到两成。
• refactoring：整锥重综合，专治跨节点公共因子，支撑变量超过 16 个时代价陡增。
• resubstitution：借已有信号表达目标节点，SAT 证明合法性后整锥消失。
• SAT sweeping：仿真分桶粗筛加 SAT 精证，图收缩正反馈，兼顾等价性检查。
• 工艺映射：cut 枚举加动态规划，抽象电路落地为标准单元，综合闭环完成。