极客工场

Appearance

共 3,816 字预计阅读约 13 分钟

LEC 等价性检查开源实测：Yosys equiv 三件套验证 RTL 与综合网表 ​

更新时间：2026-10-28。本文是「集成电路大类 · 芯片设计」中间层（intermediate）的一篇实验文。LEC 等价性检查（Logic Equivalence Checking，逻辑等价检查）回答的是一个非常具体的问题：综合工具把 RTL 变成门级网表之后，电路功能还和原来一样吗？ 商用流程里这是 Formality、Conformal 的地盘，但它们的 license 不是人人都摸得到。好消息是，对模块级、纯组合或小规模时序逻辑，开源的 Yosys 自带一套 equiv 命令族就能干这件事。本篇用一台 8 位 ALU 做一正一反两组实测：RTL 对比自家综合出的网表，9 个等价点全部 proven；再把减法故意写错一拍重跑，9 个点全部 unproven 并逐位报出。结尾诚实说清楚这套开源方案的边界在哪——哪些场景它顶得上，哪些场景必须上商用工具。关于 LEC 失败时的归因分类，可以对照阅读 LEC失败一定代表RTL有bug吗。

本文要回答的问题 ​

  • Yosys 做 LEC 的三条核心命令 equiv_make / equiv_simple / equiv_status 各自干什么？
  • gold 侧（参考设计）和 gate 侧（被检查设计）在脚本里要怎么装载，顺序错了会怎样？
  • 一次「等价 proven」的输出长什么样，一次「不等价」的输出又怎么逐位定位问题？
  • 开源方案与 Formality/Conformal 的能力边界划在哪里？

一、LEC 在流程里的位置与 Yosys 的三件套 ​

逻辑综合（逻辑综合：从 RTL 到门级网表）做的事是把行为描述的 RTL 翻译成具体门单元搭出来的网表。翻译过程会做大量变换：常数折叠、资源共享、重定时、映射到工艺库单元。每一步都可能引入 bug——综合器本身有 bug、约束写错了导致错误优化、或者 ECO 手改网表改漏了一根线。LEC 的价值就是在不跑仿真的前提下，用形式化方法（SAT 求解器）证明「对任意输入组合，两个设计的输出恒等」。仿真只能抽样，等价检查是全量。

Yosys 做这件事的流程可以画成一张对照装配图：

Yosys LEC 流程：两侧装载、配对、交给 SAT 逐位证明

这张图的关键在第 3 步：equiv_make 并不是直接比较两个模块，而是造出第三个模块 equiv，把 gold 和 gate 都实例化进去，同名输入端口接到一起，同名输出端口之间插一个 $equiv 单元——这个单元的语义就是「两端信号恒等时为 1」。于是一个「两个设计等价吗」的问题，被转化成了「这 N 个 $equiv 单元各自恒为 1 吗」的 N 个独立的 SAT 问题，交给 equiv_simple 逐个求解。这个「配对 + 插比较单元」的思路和商用工具里的 key point mapping 是同构的，只是商用工具的配对算法复杂得多。

二、实验设计：一正一反两个对照 ​

实验对象是一台刻意写得很小的 8 位 ALU，四种运算（加、减、与、或），外加一个零标志：

verilog
always @(*) begin
    case (op)
        2'd0: y = a + b;
        2'd1: y = a - b;
        2'd2: y = a & b;
        default: y = a | b;
    endcase
end
assign zero = (y == 8'h00);

设计两个对照组，是为了同时验证「该过的能过」和「该抓的能抓」——只跑 PASS 侧无法证明工具真的会报 FAIL，这在验证方法学上叫 negative test，是被 覆盖率驱动的验证 反复强调的基本功：

对照组gold 侧gate 侧预期
PASS 组simple_alu.v（RTL 原稿）alu_net.v（yosys synth 综合出的门级网表）全部 proven
FAIL 组simple_alu.vsimple_alu_bad.v（a-b 故意写成 a-b-1）全部 unproven，逐位报出

先用 mknet.ys 把 RTL 综合成网表——注意这个网表没有映射到具体工艺库，是 yosys 内部通用门（$add、$pmux 这类 RTLIL 单元）组成的网表，这对 LEC 来说反而更公平：两侧用同一套单元语义，SAT 模型里没有库单元真值表这层噪音。还可以提前算一笔账：这个设计的输出是 8 位的 y 加 1 位的 zero，equiv_make 按输出线网逐位插比较单元，所以最后应该恰好看到 9 个 $equiv 点——后面两次跑出来的计数如果对不上这个预期，说明配对阶段就出了问题，比如端口名对不齐导致某些输出根本没被纳入比较，那种「全绿」是假的。

三、PASS 组实录：9 个等价点全部 proven ​

lec_pass.ys 的完整内容只有八行，但每一行的顺序都不能乱：

tcl
read_verilog simple_alu.v
prep -top simple_alu
rename simple_alu gold
read_verilog alu_net.v
rename simple_alu gate
equiv_make gold gate equiv
equiv_simple
equiv_status

这里埋着全篇第一个坑：gold 侧必须先跑 prep（或至少 proc）再 rename。always @(*) 块在 yosys 内部表示为 process（过程块），而 equiv_make 只接受纯网表形态的模块——如果跳过 prep 直接 rename 再 equiv_make，工具会直接报错「Gold module contains memories or processes」。先 prep -top 把过程块展平成多路选择器和逻辑门，gold 侧才具备被比较的资格。

跑完的真实输出核心段：

PASS 组：9 个 $equiv 单元全部 proven

这段实录读法分三层。第一层是 EQUIV_MAKE 阶段的配对报告：a_gold 与 a_gate 配成一对输入、y_gold 与网表里那串综合出来的 $ternary/$not 单元输出配成一对输出——注意 y 的 gate 侧已经不是一根线，而是综合后 8 个三态门输出的拼接，这正是综合变换留下的痕迹，LEC 要证明的就是「这一坨门」和原来的 case 语句行为恒等。第二层是 EQUIV_SIMPLE 阶段：9 个 $equiv 单元（y 的 8 个 bit 加 zero 共 9 个比较点）逐个 Trying to prove ... success!，SAT 求解器对每个点都证明了「找不到任何输入组合使两端不同」。第三层 EQUIV_STATUS 汇总：9 are proven and 0 are unproven. Equivalence successfully proven!，进程退出码 0——这个退出码是把它接进 CI 的关键，脚本可以机械地根据退出码放行或拦截综合结果。

把最要紧的几行原样摘录，方便逐字核对：

exp-log
5. Executing EQUIV_SIMPLE pass.
Found 9 unproven $equiv cells (2 groups) in equiv:
  Trying to prove $equiv for \zero: success!
 Grouping SAT models for \y:
  Trying to prove $equiv for \y [0]: success!
  ...
  Trying to prove $equiv for \y [7]: success!
Proved 9 previously unproven $equiv cells.

6. Executing EQUIV_STATUS pass.
Found 9 $equiv cells in equiv:
  Of those cells 9 are proven and 0 are unproven.
  Equivalence successfully proven!
YOSYS_EXIT=0

有一个细节值得注意：equiv_simple 把 y 的 8 个 bit 归为「一组」（Grouping SAT models for y），zero 单独一组。分组的意义是 SAT 求解器可以在同组内复用反例模型加速——一个点证完后得到的结构信息能缩小同组其他点的搜索空间。整个证明真实耗时在日志尾部：CPU user 0.06 秒、内存峰值 22.77 MB。对这种规模的设计，等价检查的成本低到可以每次综合后随手跑一次。

四、FAIL 组实录：一拍之差，9 个点全部抓出 ​

现在做 negative test。simple_alu_bad.v 里把减法写成 y = a - b - 8'd1——差一错误（off-by-one），硬件 bug 里最常见的类型之一。脚本也要跟着调整，这是全篇第二个坑：

tcl
read_verilog simple_alu.v
proc simple_alu
opt simple_alu
rename simple_alu gold
read_verilog simple_alu_bad.v
proc simple_alu_bad
opt simple_alu_bad
rename simple_alu_bad gate
equiv_make gold gate equiv
equiv_simple
equiv_status

为什么这里不能照抄 PASS 组的 prep -top？因为 prep -top 会清理「顶层用不到的所有模块」——第二次 read 之后如果再 prep -top simple_alu_bad，已经被 rename 成 gold 的模块会被当作无用模块删掉，后面 equiv_make 就找不到 gold 了。所以 FAIL 组改成按模块名分别跑 proc 和 opt：只展平过程块、做基础优化，但不做层级清理。这个坑的教训是通用的：在 yosys 脚本里，凡是带「清理」语义的命令（prep/clean/purge），在多模块共存场景下都要想清楚它会不会误伤。

FAIL 组的真实输出：

FAIL 组：9 个 $equiv 单元全部 unproven，逐位报出

读法和 PASS 组正好镜像：equiv_simple 里 9 个 Trying to prove ... failed.，Proved 0 previously unproven $equiv cells；equiv_status 汇总 0 are proven and 9 are unproven，然后逐行列出每个未证明点的两侧信号名：y_gold [7] 对 y_gate [7] 一路到 y [0]，外加 zero_gold 对 zero_gate。zero 为什么也不等价？因为 zero = (y == 8'h00)，y 错了 zero 自然跟着错——这个「连带失败」本身就是定位线索：排查时可以先看哪些失败点是其他失败点的下游组合逻辑，真正的 bug 往往藏在最上游那一簇。

值得说透的是「failed」的确切语义：SAT 求解器找到了至少一个输入组合使两端输出不同（比如 op=1、a=5、b=3 时 gold 输出 2、bad 输出 1）。也就是说 unproven 在这里等于「证伪并握有反例」，不是「证明超时没结论」。equiv_simple 默认不会把反例展开打印，想要反例激励可以追加 equiv_induct 或换 sat -verify 手工求解——但对「抓住 bug」这个目标，equiv_status 的逐位清单已经足够指导回 RTL 里定位了。

两组对照合起来，这个实验的自洽性就闭环了：同一个工具、同一个 gold，换上网表全过、换上差一错误的版本全抓——工具有区分度，结论才可信。这也是 LEC失败一定代表RTL有bug吗 里反复强调的前提：先确认检查环境本身可信，再谈归因。

五、诚实划界：开源 equiv 与 Formality/Conformal 差在哪 ​

做到这里，很容易产生「开源够用了」的乐观结论。必须把边界划清楚。Yosys equiv 这套流程在本实验里表现完美，但它和商用 LEC 工具的能力差距是实打实的：

开源 Yosys equiv 与商用 LEC 的能力边界

这张表里最重的一行是「重定时（retiming）」。一旦综合器或手动优化移动了寄存器位置，两个设计的时序点对齐了但拍级结构变了，简单的 $equiv 配对会立刻全灭——商用工具靠时序感知的 mapping 算法解决这个问题，yosys 的 equiv_make 做不到。所以本篇实验的正确打开方式是：把 yosys LEC 当成模块级的「综合哨兵」——每次修改 RTL 重综合后跑一次，秒级成本挡住「综合脚本或约束把设计改坏了」这类事故；而涉及签核、工艺映射网表、大规模设计的最终确认，仍然交给商用工具。这与 芯片验证全景 里「形式验证分层使用」的思路一致：不同规模的验证问题用不同档位的工具，不追求一把锤子敲所有钉子。

六、接进 CI：equiv 命令族的其余成员与退出码纪律 ​

本实验只用了三条 equiv 命令，但 equiv 家族还有几个成员值得知道，它们分别对应「更难的设计怎么收敛」这一串递进问题：

命令干什么什么时候用
equiv_make配对两侧同名线网，造出插满 $equiv 单元的 equiv 模块每次必用
equiv_simple对每个未证明点跑一轮 SAT，适合组合逻辑默认第一站
equiv_induct对时序等价点做归纳证明（k-induction）含寄存器的时序等价
equiv_mark把已证明点的前后驱动结构标记出来，缩小剩余问题大设计分治
equiv_remove移除已证明点，把难啃的留给更重的引擎与 equiv_simple 迭代配合
equiv_status -assert存在未证明点时直接让脚本失败CI 拦截的最后一道

把这个塞进 CI 的最小形态只有几行 shell——综合、等价检查、按退出码拦截，一气呵成：

bash
#!/bin/bash
set -e
yosys mknet.ys            # 重综合，产出最新网表
yosys lec_pass.ys         # 等价检查；equiv_status 确认全 proven 后退出码为 0
echo "LEC PASS, netlist cleared for downstream"

退出码纪律是这套用法里最容易被忽视的一环。本次 PASS 跑日志末尾的 YOSYS_EXIT=0 不是装饰：yosys 脚本执行到 equiv_status 发现全部 proven 时进程正常结束；而在带 -assert 的变体或严格模式下，存在 unproven 点会直接以非零退出。CI 里只要 set -e 或者显式判断 $?，综合改坏设计的提交就会在合并前被拦下。这套「秒级形式化哨兵」的成本有多低，日志里的数字可以作证：PASS 跑 CPU user 0.06 秒、常驻内存 12.76 MB，FAIL 跑更是只有 0.02 秒——比编译一次 RTL 还便宜。在开源项目里，没有任何理由不把它挂成每次 push 的默认检查。

还有一个使用经验的提醒：当设计长大到 equiv_simple 开始超时，第一反应不应该是「换商用工具」，而是先用 equiv_mark 加 equiv_remove 做分治——已证明的部分从问题里剥掉，剩下的 SAT 实例往往小一个数量级。只有当配对本身失败（改名、重定时、工艺映射）或者规模到了商用工具的分层算法才吃得动的量级，才到了上一节表格里「必须商用」的那一行。

这一篇在知识体系里的位置 ​

一句话总结 ​

LEC 等价性检查不一定需要商业 license 才能上手：Yosys 的 equiv_make/equiv_simple/equiv_status 三件套，配合「gold 侧先 prep、多模块不用 prep -top」两条脚本纪律，就能把模块级的 RTL 与综合网表等价检查跑通——本篇实测 8 位 ALU 正反对照：网表组 9 个等价点全部 proven、退出码 0，差一错误组 9 点全部 unproven 并逐位报出 y[7:0] 与 zero；但重定时、工艺映射网表、大规模签核仍是 Formality/Conformal 的地盘，开源方案的正当定位是模块级 CI 里的「综合哨兵」。

实验环境 ​

  • 机器/系统：云主机 / Ubuntu 22.04（eda-golden-v1 镜像）
  • 工具版本：Yosys 0.9（git sha1 1979e0b，版本行照抄日志头部）
  • 日期：2026-10-28
  • 完整命令序列：yosys mknet.ys（综合产 alu_net.v）→ yosys lec_pass.ys（RTL vs 网表，预期 PASS）→ yosys lec_fail.ys（RTL vs 错版，预期 FAIL）

代码获取 ​

完整 RTL、错版、三个 yosys 脚本与三份原始日志已同步到公开仓库：geek-doc.cn/experiments/lec-yosys-equiv-opt，克隆后进入该目录依次执行 yosys mknet.ys && yosys lec_pass.ys && yosys lec_fail.ys 即可复现本文全部结果。