Yosys 等价性检查：equiv_make 拼 miter、equiv_simple 证明、equiv_status 出结论

更新时间：2026-11-04。改 RTL 是日常：条件表达式换种写法、case 改成移位、合并两个分支——改完凭什么相信功能没变？仿真只能覆盖你想到的向量，而 Yosys 的第一次综合之后还要面对「综合器优化有没有改坏功能」。Yosys 等价性检查（Combinational Equivalence Checking，组合等价检查）用 SAT 求解器对所有输入组合做穷尽证明，不靠测试向量。本篇用 Yosys 0.33 真跑一条完整流程：equiv_make 拼 miter、equiv_simple 证明、equiv_status 出结论，并故意制造一处改写错误看它怎么报。

本文要回答的问题

equiv_make / equiv_simple / equiv_status 三个 pass 各干什么，为什么缺一不可？
miter 电路是什么结构，凭什么能证明两份设计等价？
golden 是行为 RTL、revised 是综合后的门级网表，两者写法完全不同也能比吗？
报告里的 $equiv cell、proven / unproven 分别是什么意思？
改写确实引入 bug 时，输出长什么样、退出码怎么用于持续集成？

一、Yosys 等价性检查在流程里的位置：形式验证卡在哪一步

等价性检查是一道不依赖仿真向量的验证关卡。上游给它两份设计：golden（黄金参考，通常是确认过的旧版 RTL）与 revised（改写后的 RTL，或它综合出的网表）；它产出的不是文件，而是一句结论——每个输出端「已证明等价」或「无法证明」。关卡可以放在 RTL 重构之后、综合优化之后、甚至 ECO 手工改网表之后。

读这张卡抓住「两份输入、三个 pass」：前两步把两份设计收进同一个 Yosys 会话，真正的检查只有后三个 pass。本簇的 Yosys 脚本文件组织讲过怎么把这类流程存成 .ys 复用；本篇的两个脚本 eq.ys / neq.ys 就是照这个套路写的。

miter 的结构可以用一张小图说清：两份电路并列摆放，同名输入焊在一起保证喂的是同一个激励，同名输出各接一个异或比较器——只要存在任何一组输入让两个输出不一致，比较器就可能翻转，SAT 求解器就去找这组输入；找不到，才叫证明。

读图注意两侧抽象级别不同：golden 是没综合的行为代码，revised 侧已经是 8 个 $_ 通用门。等价性检查比的是布尔函数，不关心你用 case 还是移位实现——这正是它能做「综合前后对比」的原因。

二、命令逐段解读：eq.ys 的九个步骤

完整脚本只有十几行，分三段：

bash

read_verilog golden.v
prep -top decoder
splitnets -ports
design -stash gold

read_verilog revised.v
synth -flatten -top decoder
splitnets -ports
design -stash gate

design -copy-from gold -as gold decoder
design -copy-from gate -as gate decoder
equiv_make gold gate miter
equiv_simple miter
equiv_status -assert miter

命令	作用	不写会怎样
`prep -top decoder`	跑 hierarchy/proc/opt 等准备 pass，把行为 RTL 化成布尔逻辑	golden 侧若残留 `always`/case，equiv_make 无法按门比较
`splitnets -ports`	把多位端口拆成 1 位标量	两侧按位配对时错位，同名线网匹配不上
`design -stash gold`	把当前设计收进名为 gold 的「抽屉」并腾空工作区	读第二份文件会报模块重复定义
`synth -flatten`（gate 侧）	把 revised 真正综合成门级、展平层次	比的就是 RTL 对 RTL，演示不了「综合前后」
`design -copy-from gold -as gold decoder`	从抽屉取出模块并重命名为 gold	两份模块都叫 decoder，不改名无法共存
`equiv_make gold gate miter`	生成名为 miter 的检查模块，输入短接、输出插 `$equiv`	没有 miter，后两个 pass 无对象可查
`equiv_simple miter`	对每个未证明的 `$equiv` 调 SAT/AIG 后端尝试证明	全部 `$equiv` 停留在 unproven 状态
`equiv_status -assert miter`	汇总并在有未证明单元时让 Yosys 以非零码退出	失败只打印报告，脚本退出码仍是 0，CI 拦不住

三个 pass 的分工就是「搭台子 → 证明 → 宣判」。equiv_make 只做结构拼接，不做任何数学证明，日志里它干的事是逐对打印 Presumably equivalent wires；equiv_simple 才是算力大头，它对每个输出把两侧的组合逻辑锥摘出来交给 SAT；equiv_status 纯统计。还要区分 failed 的两种语义：SAT 找到了让两侧输出不一致的输入，是「确定不等价」；设计太大、求解超时则是「证明不了」，同样计入 unproven 但含义完全不同——前者回去改代码，后者可以加 -nogood/-undef 等选项或拆小模块重试。注意这套流程针对组合逻辑。含寄存器的设计要给 equiv_simple 加 -seq N -set-at 1 ... 做顺序展开，那属于 SEC 时序等价的地盘。另一个近亲是 equiv_opt，它用来证明「某个优化 pass 本身」没改语义，本篇不展开。

三、输入输出文件：两份 RTL 与内存中的 miter

实验设计是一个带使能的 2-4 译码器。golden 用最朴素的 case：

verilog

module decoder (
    input  wire [1:0] sel, input wire en,
    output reg  [3:0] y
);
    always @(*) begin
        y = 4'b0000;
        if (en) case (sel)
            2'b00: y = 4'b0001; 2'b01: y = 4'b0010;
            2'b10: y = 4'b0100; 2'b11: y = 4'b1000;
        endcase
    end
endmodule

revised 改成一行移位写法——sel 取 0 到 3 时，1 << sel 正好是四种独热码，功能应当完全相同：

verilog

module decoder (
    input  wire [1:0] sel, input wire en,
    output wire [3:0] y
);
    assign y = en ? (4'b0001 << sel) : 4'b0000;
endmodule

喂给流程的是这两个 .v；miter 不自动落盘，它活在 Yosys 内存里，由 2 个子模块、短接输入和 4 个 $equiv 单元组成。需要交付或肉眼检查时可在 equiv_make 后加 write_verilog miter.v 导出。形式证明与仿真的根本差别也在这个结构里：仿真要你自己给激励，8 种输入组合最多写 8 行测试；SAT 直接回答「是否存在一组输入让比较器翻转」，一次求解覆盖全部组合，设计从 3 个输入扩到 30 个输入也不需要补测试向量——这正是改 RTL 重构时用它兜底的原因。equiv_make 的配对规则是同名：同名输入短接、同名输出插比较器，所以两侧端口名必须一致，内部信号叫什么无所谓。本例日志明确配对了 7 对端口（y[3:0]、sel[1:0]、en）。

四、常见错与检查点

现象	先查什么	纠正
`ERROR: Module 'gold' not found!`	stash 名字和 `design -copy-from` 引用是否一致、模块是否 `-as` 重命名	三个名字（stash 名、取出后的新名、equiv_make 参数）对齐
`Found 0 $equiv cells`，结论永远「通过」	两侧端口名是否对不上、是否漏了 `splitnets -ports`	输出必须同名同位宽；两侧都跑 `splitnets -ports`
revised 已映射到厂商标准单元，miter 里全是未识别 cell	gate 侧是否做了 techmap	停在 `$_` 通用门比对，或给 equiv_make 加 `-map +/equiv/cmos/cells_sim.v` 提供单元仿真模型
设计含触发器却按本篇脚本跑，大量 unproven	是否把时序问题当组合问题证	用 `equiv_simple -seq N -set-at` 展开，或转 SEC 流程
CI 里明明不等价流水线却绿灯	是否加了 `-assert`	持续集成场景必须用 `equiv_status -assert`，靠退出码而非日志文本判断

一个实用检查动作：先看 equiv_make 打印的配对清单是不是你预期的端口数。本例 3 个输入、4 个输出共 7 对；数量就不对，后面的证明再漂亮也没有意义。

五、真实跑一遍：等价例与故意写错例

在 geek-eda:0.4-flow 容器里跑 bash run.sh（等价于依次执行两个 .ys）。等价例最后三个 pass 的真实输出：

实录里 equiv_simple 对 y[3] 到 y[0] 逐一点名，四个都是 success!，equiv_status 汇总为 4 are proven and 0 are unproven，最后一行 Equivalence successfully proven!，退出码 0。至此「case 写法」和「移位写法 + 综合」在全部 8 种输入组合下功能一致，是被穷尽证明的，不是仿真碰出来的。

再看反例。把禁用时的输出故意改成 4'b0001（buggy.v），其余不动，SAT 立刻定位到最低位无法证明：

exp-log

8. Executing EQUIV_SIMPLE pass.
Found 4 unproven $equiv cells (4 groups) in miter:
  Trying to prove $equiv for \y[3]: success!
  Trying to prove $equiv for \y[2]: success!
  Trying to prove $equiv for \y[1]: success!
  Trying to prove $equiv for \y[0]: failed.
Proved 3 previously unproven $equiv cells.

9. Executing EQUIV_STATUS pass.
Found 4 $equiv cells in miter:
  Of those cells 3 are proven and 1 are unproven.
  Unproven $equiv ...find_same_wires$139: \y[0]_gold \y[0]_gate
Found a total of 1 unproven $equiv cells.

注意三件事：第一，y[3:1] 仍然证明成功，unproven 精确落在 y[0]——正是 en=0 时两版唯一有分歧的那一位；第二，failed 不等于工具出错，它的含义是「SAT 找到了反例（或证明不了）」，即两版确实不等价；第三，neq.ys 故意不用 -assert，所以脚本退出码仍是 0、日志完整打印，而生产脚本应带 -assert 让这种情况直接返回非零码。报告 unproven 之后怎么反推到具体输入和 RTL 行，是不等价调试套路的主题。

实验环境

机器/系统：macOS（Darwin 25.5，Apple Silicon），容器镜像 geek-eda:0.4-flow（Docker）
工具版本：yosys -V 输出 Yosys 0.33 (git sha1 2584903a060)，容器内置 SAT 后端
日期：2026-11-04
完整命令：docker run --rm -v "$PWD":/work -w /work geek-eda:0.4-flow yosys -V → ... yosys -s eq.ys（等价例）→ ... yosys -s neq.ys（不等价例）；等价于在实验目录执行 bash run.sh 或 make run

代码获取

完整 RTL、两个 Yosys 脚本与 Makefile 已同步到公开仓库：geek-doc.cn/experiments/flow-yosys-equiv-check，克隆后进入该目录执行 make run 即可在 geek-eda:0.4-flow 容器中连续复现等价例（EQUIVALENT，退出码 0）与不等价例（1 个 unproven $equiv）。

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

想先弄清综合本身在做什么、为什么综合前后值得做 Yosys 等价性检查：读 Yosys 的第一次综合与 synth 命令解剖；
想把这套检查接进网表交付环节：读 Yosys 网表输出流程；
寄存器搬移、流水线重切后组合等价失效：读 SEC 时序等价与 LEC 等价性检查与 Formality；
报告 unproven 之后怎么定位到具体输入和代码行：读不等价调试套路。

总结

Yosys 等价性检查的完整套路是「两份设计、三个 pass」：先用 prep/synth -flatten 加 splitnets -ports 分别备好 golden 与 revised 并用 design -stash 隔离，再 design -copy-from 取出重命名；equiv_make 把同名输入短接、每对同名输出插一个 $equiv 比较器拼成 miter；equiv_simple 对每个输出的组合逻辑锥调 SAT 穷尽全部输入；equiv_status 汇总 proven/unproven 并宣判。实测中 case 写法与移位写法的译码器 4 个输出全部证明成功，而把禁用输出改错一位后，unproven 精确落在 y[0]。记住三条：配对靠同名端口、组合逻辑才能直接这样证、CI 里一定加 -assert 靠退出码拦截不等价。

入门

进阶

专家

Yosys 等价性检查：equiv_make 拼 miter、equiv_simple 证明、equiv_status 出结论 ​

本文要回答的问题 ​

一、Yosys 等价性检查在流程里的位置：形式验证卡在哪一步 ​

二、命令逐段解读：eq.ys 的九个步骤 ​

三、输入输出文件：两份 RTL 与内存中的 miter ​

四、常见错与检查点 ​

五、真实跑一遍：等价例与故意写错例 ​

实验环境 ​

代码获取 ​

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

总结 ​