Yosys sat 命令：不依赖 sby 的内建 SAT 属性证明与证明深度陷阱
更新时间：2026-11-14。仿真是给输入、看输出，输入空间再大也只能覆盖你想到的向量；形式证明换了个问法——「是否存在一组输入让属性不成立」，一次求解穷尽所有可能。Yosys sat 命令（内建
satpass）不用装 SymbiYosys（sby）、不用写.sby工程文件，一行命令就能对小模块做属性证明。本篇在 Linux 容器里用 Yosys 0.33 真跑四类实验：组合属性的正例与反例、时序计数器属性的深度扫描，并把两个工程坑（证明深度不够会假通过、FAIL 时退出码仍是 0）讲透。同系列的 Yosys 手工 pass 链 解决「综合流程怎么排」，Yosys 等价性检查 解决「两份设计是否等价」，本篇解决「单个模块的一条属性是否成立」。
本文要回答的问题
sat -prove eq 1到底在证明什么，SUCCESS和FAIL两行 verdict 各自的数学含义是什么？-set-def-inputs为什么不能省，它给 SAT 问题加了什么约束？- 时序电路用
sat -seq N展开，为什么错误实现在深度 1 会假通过、深度 2 才被抓出来？ - 证明报告 FAIL 了，
echo $?却是 0，持续集成里到底该怎么判？ - 内建
sat与 miter 等价检查、SymbiYosys 各自的适用边界在哪？
先给一张全篇流程图，后面各节按这五步展开：
一、Yosys sat 命令在证明什么：找反例，而不是跑向量
先把判定语义钉死，因为它和仿真的直觉是反的。sat pass 把设计展开成布尔公式，连同你给的证明约束一起丢给 SAT 求解器，求解器的任务不是「验证属性成立」，而是寻找一组让属性不成立的输入（反例模型）。
| 判定行（日志原文） | 求解器含义 | 工程结论 |
|---|---|---|
SAT proof finished - no model found: SUCCESS! | 在给定范围内不存在反例 | 属性成立，证明通过 |
SAT proof finished - model found: FAIL! | 找到了反例，并打印该输入下各信号取值 | 属性被证伪，照反例表回去改 RTL |
关键在 no model found 这几个字：不是「测了很多向量都过了」，而是「反例不存在」这件事本身被求解器判定为不可满足。反过来，只要反例存在，SAT 一定会把它找出来并连信号赋值一起给你，不存在「漏检」，只存在「范围没覆盖到」——第三节会看到范围（证明深度）不够时，反例确实存在却落在观察窗口之外。
一次完整证明的数据流可以分成三段：准备约束、求解、按 verdict 分流。
读这张图抓住颜色分工：蓝色是准备动作，橙色是真正的求解计算，红色节点是判定分叉与证伪出口，绿色是证明成立出口，紫色提醒自动化收口不能靠退出码。Yosys sat 命令的所有参数都是在给「证明准备」这一层添约束，下面两节逐个拆。
二、组合属性：-set-def-inputs 与正反例实测
实验模块小到可以一眼看完。prop_good 里 y1 = a ^ b、y2 = ~(a ^ b)，按布尔代数 y2 == ~y1 恒成立，属性信号 eq 应当永远为 1：
module prop_good(input a, input b, output y1, output y2, output eq);
assign y1 = a ^ b;
assign y2 = ~(a ^ b);
assign eq = (y2 == ~y1);
endmodule证明命令只有一行，注意 -set-def-inputs 和 -prove eq 1 两个参数：
yosys -p "read_verilog rtl/prop_good.v; sat -set-def-inputs -prove eq 1 prop_good"-prove eq 1 的意思是把 eq = 1'1 作为证明约束加进公式——日志里对应 Import proof-constraint: \eq = 1'1，求解器随后去找让这条约束不成立的输入。-set-def-inputs 解决的是「输入端口取什么值」的问题：它让模块输入在 SAT 问题里自由取默认值（def constraint），日志中对应两行 Import def constraint for this timestep: \a、\b。省掉它，输入没有取值自由度，证明退化成对一个固定态的检查，结论没有意义。
正确模块的 verdict 没有任何悬念：
实录第 7 行 no model found: SUCCESS! 说明：输入 a、b 一共只有四种组合，求解器逐一在公式层面判定，不存在任何一种让 eq=0，属性成立。接着故意注入一个错误，把第二式的异或写成与：
module prop_bad(input a, input b, output y1, output y2, output eq);
// 故意注入错误：第二式把异或写成了与，eq 不再恒成立
assign y1 = a ^ b;
assign y2 = ~(a & b);
assign eq = (y2 == ~y1);
endmodule同一条命令这次得到 model found: FAIL!，反例表直接点名 \a = 1、\b = 1、比较器 $eq...Y = 0。手工验证：a=b=1 时 y1=0、~y1=1，而 y2=~(1&1)=0，两边不等，反例成立。这就是形式证明相对仿真的价值——不需要你想到「11 这个向量会不会有问题」，求解器把它送上门。反例表的读法是先看输入列（复现条件），再顺着比较器输出定位到具体 RTL 行。
三、时序属性与证明深度：深度 1 的假通过
带触发器的设计，单时间框装不下「逐拍」语义。sat 用 -seq N 把电路按时间步展开 N 拍，属性在每个时间步都必须成立。实验对象是两个 4 位计数器，正确版两个寄存器每拍都加 1，eq = (a == b) 应当逐拍为真：
module seq_good(input clk, output [3:0] q1, output [3:0] q2, output eq);
reg [3:0] a, b;
initial begin a = 4'd0; b = 4'd0; end
always @(posedge clk) a <= a + 4'd1;
always @(posedge clk) b <= b + 4'd1;
assign q1 = a;
assign q2 = b;
assign eq = (a == b);
endmodule两个细节先说明。第一，时序证明前要先跑 proc 把 always/initial 展平，完整命令是 read_verilog rtl/seq_good.v; proc; sat -seq 4 -prove eq 1 seq_good。第二，initial 给的初值不是可有可无：没有它，初态未被约束，求解器可以任选寄存器上电值，反例平凡化，探针实测去掉 initial 后所有深度都报 FAIL。另外字面量必须写 4'd1 这种完整位宽形式，写成 4d1 会直接被解析器判语法 ERROR。
把证明深度从 1 扫到 4，两个模块的实测结果如下：
| 模块 | seq=1 | seq=2 | seq=3 | seq=4 |
|---|---|---|---|---|
seq_good（两计数器都加 1） | SUCCESS | SUCCESS | SUCCESS | SUCCESS |
seq_bad（第二个每拍加 2） | SUCCESS（假通过） | FAIL | FAIL | FAIL |
seq_bad 只改了一行：b <= b + 4'd2。第一拍结束时 a=1、b=2 之前，两个寄存器在第 0 拍都是初值 0，深度 1 的观察窗口里故障还没显现，于是求解器诚实地报告「窗口内无反例」——这就是假通过：不是工具判错，是你给的深度够不到故障拍。深度加到 2，第二拍 a=1、b=2，eq 第一次为 0，反例立刻被抓住。结论很直接：证明深度必须覆盖故障延迟，对 N 拍流水线、计数器比对一类属性，深度至少要等于状态发散所需的拍数，工程上习惯从 1 开始向上扫到 FAIL 收敛或深度预算上限。
深度 4 的完整反例表按时间步组织，规模是 451 variables and 1228 clauses：
Solving problem with 451 variables and 1228 clauses..
SAT proof finished - model found: FAIL!
Time Signal Name Dec Hex Bin
---- ---------------------------- ----------- --------- -------------
init \a 0 0 0000
init \b 0 0 0000
---- ---------------------------- ----------- --------- -------------
1 $eq$rtl/seq_bad.v:9$5_Y 1 1 1
---- ---------------------------- ----------- --------- -------------
2 $eq$rtl/seq_bad.v:9$5_Y 0 0 0
---- ---------------------------- ----------- --------- -------------
3 $eq$rtl/seq_bad.v:9$5_Y 0 0 0
---- ---------------------------- ----------- --------- -------------
4 $eq$rtl/seq_bad.v:9$5_Y 0 0 0init 行确认两寄存器从 0 出发；时间步 1 比较器还是 1，第 2 拍起变 0 并保持——与「加 2 的计数器第二拍发散」的手工推演逐拍吻合。读时序反例表要纵向看同一个信号跨时间步的变化，而不是横向扫某一拍。
四、退出码陷阱：FAIL 了，$? 仍然是 0
这是最容易在持续集成里出事的坑。实录第 22 行白纸黑字：prop_bad 已经被判 FAIL!，紧接着的 yosys 退出码=0。也就是说 sat 证明失败只体现在日志文本里，不体现在进程退出码上，脚本里写 if yosys ...; then echo OK 会把证伪的设计当通过放过去。
正确做法是把 verdict 文本抓出来判，实验脚本 run.sh 末尾的汇总段就是这个模式：
for f in build/comb_good.log build/comb_bad.log build/seq_bad_seq4.log; do
printf '%-28s %s\n' "$f" "$(grep -oE 'SAT proof finished - .*(SUCCESS|FAIL)!' "$f")"
done工程化时再加一步：grep 到 FAIL! 就以非零码退出脚本，让 CI 真正红掉。注意这与 Yosys 等价性检查 里的 equiv_status -assert 是同一类问题的两种解法——那边有 -assert 选项把失败映射成退出码，内建 sat 没有等价开关，只能自己解析文本。
五、边界与误区：什么时候不该用内建 sat
| 场景 | 内建 sat 适不适合 | 原因与替代 |
|---|---|---|
| 几十到几百个单元的小模块属性 | 适合 | 公式规模小，秒级出结果，无需额外工程 |
| 两份 RTL/网表的输出等价 | 不用本篇流程 | 走 equiv_make+equiv_simple 的 miter 工作流，见等价性检查篇 |
| 含触发器的设计按单时间框证明 | 禁止 | 触发器会被当成自由输入，假通过；必须 proc 后加 -seq N |
| 大规模设计、多属性、需 cover/assume 管理 | 不适合 | 转 SymbiYosys 工程，用 sby 组织属性文件与求解后端 |
| 寄存器无初值的时序证明 | 先补初值 | 初态未约束时反例平凡化，结论不反映真实上电行为 |
还要澄清本篇与姊妹篇的错位：Yosys 等价性检查 的 miter 流程回答「两份实现是否逐输出等价」，输入是两份设计、产物是 proven/unproven 清单；本篇的 Yosys sat 命令回答「一份实现的一条属性是否存在反例」，输入是单模块加 -prove 约束。探针中实测过一个反面用法：对时序电路直接套 miter -equiv 加单时间框 sat，触发器被当作自由输入，错误设计也能拿到 SUCCESS——时序问题必须交给 -seq 展开，或走 SEC 时序等价 的专门流程。
实验环境
- 机器/系统：linux/amd64 容器，Ubuntu 24.04
- 工具版本：
yosys -V输出Yosys 0.33 (git sha1 2584903a060)，内建 SAT 后端 - 日期：2026-11-14
- 完整命令：实验目录下执行
bash run.sh；脚本依次跑组合属性正反例、sat -seq 1..4深度扫描、seq=4 完整反例表与 verdict 汇总，各次完整日志落在build/
代码获取
完整 RTL、run.sh 与 README 已同步到公开仓库：geek-doc.cn/experiments/yosys-sat-proof，克隆后进入该目录执行 bash run.sh 即可连续复现组合属性 SUCCESS/FAIL 两例、时序属性四个深度的扫描结果与退出码观察。
这一篇在知识体系里的位置
- 还没建立「RTL 怎样沉降为门电路」的整体直觉：先读 Yosys 入门：综合把 RTL 变成了什么；
- 想理解
sat之外的 pass 怎么手工编排、proc在 pass 链里处于什么位置：读 Yosys 手工 pass 链 与 Yosys 脚本文件组织； - 任务是比对两份设计而非证明单条属性：读 Yosys 等价性检查，拿到 FAIL 后怎么反推代码行读 不等价调试套路；
- 属性涉及多拍流水线、需要正式的时序等价 sign-off：读 SEC 时序等价 与 LEC 等价性检查与 Formality。
总结
Yosys sat 命令是不依赖 SymbiYosys 的轻量形式证明工具：-set-def-inputs 放开输入取值、-prove eq 1 声明证明目标，求解器通过「找反例」给出 verdict——no model found: SUCCESS! 是反例不存在、属性成立，model found: FAIL! 是反例被连同样例赋值一起给出。实测中组合属性正反例都符合布尔推演，而时序计数器实验暴露了两个必须记住的工程点：证明深度要覆盖故障延迟，错误实现在 seq=1 假通过、seq=2 才被抓；FAIL 时进程退出码仍是 0，自动化只能 grep verdict 文本判定。小模块属性证明用内建 sat，两份设计等价走 miter，大规模多属性体系再上 SymbiYosys——按问题规模选工具，别拿一把锤子敲所有钉子。