sby smtbmc 证明超时：depth 调参、bmc 降级与引擎切换的结论误读排查

更新时间：2026-11-05。报错排查篇，属于 EDA 报错排查系列。很多人第一次跑 SymbiYosys（sby）的 smtbmc 引擎，看到 DONE (FAIL, rc=2) 就以为设计被证伪、看到 DONE (PASS, rc=0) 就以为属性被证明，两种读法都可能是错的。本篇用一个 4 位计数器的四组对照实测把结论摆清：同一个目标状态 cnt == 10，cover 模式 depth 3 报 FAIL、depth 12 报 PASS；同一条断言 bmc 模式 depth 3 报 PASS、depth 12 报 FAIL 并落盘反例。变化的只有 depth 这一个参数。断言与形式化验证的基础概念可以先读 SVA 断言基础的 sby 实证，本篇专注「结论怎么读、参数怎么调」。

首屏答案：sby 配置里的 depth 是检验步数（拍数）的上界，不是求解器的墙钟超时时间。cover 模式的 FAIL（rc=2）含义是「在 depth 划定的拍数窗口内目标状态不可达」，不代表目标恒假，第一反应是算清目标最早第几拍可达、把 depth 加到覆盖它；bmc 模式的 PASS（rc=0）含义是「界内没找到反例」，只是有界结论，想要任意深度都成立的强结论要换 mode prove 让 smtbmc 做时序归纳。真正的墙钟超时在日志里是 timeout 字样、结论归 unknown（返回码 3），与 rc=2 不是一类问题。

读这张卡抓住一个判别顺序：拿到 sby 结论先看 [options] 里的 mode，再看 depth，最后才读 PASS/FAIL。前两栏同为 rc=2 的 FAIL，cover 下是「没够着」、bmc 下是「被抓包」，语义恰好相反；第三栏的 PASS 最容易给人虚假的安全感，它的完整翻译是「在给定拍数内暂未发现反例」。本篇四组实验就是把这三栏逐条跑成真实日志。

本文要回答的问题

• sby 配置里的 depth 到底限制的是什么？它和求解器的墙钟超时是不是一回事？
• cover 模式跑出 Unreached cover statement 加 DONE (FAIL, rc=2)，能说明目标状态不可达吗？
• bmc 模式的 PASS 为什么只是有界结论？想要「任意深度都成立」该怎么配？
• 同样一条断言，为什么 depth 3 报 PASS、depth 12 反而报 FAIL？
• 什么情况下才需要把 smtbmc 的求解器从 z3 换成 yices 或 boolector？

一、现象原文：四组对照，变量只有 depth

被测设计小到可以全文贴出。一个 4 位计数器每拍加 1，目标状态 cnt == 10 最早第 11 拍才可达（复位后 cnt 从 0 开始，连续加 10 次）：

// cover.v：cover 形式，问「cnt==10 能不能到达」
module top (input clk);
    reg [3:0] cnt = 0;
    always @(posedge clk) begin
        cnt <= cnt + 4'd1;
        cover(cnt == 4'd10);
    end
endmodule

// reach.v：assert 形式，问「cnt!=10 能不能永远守住」
module top (input clk);
    reg [3:0] cnt = 0;
    always @(posedge clk) begin
        cnt <= cnt + 4'd1;
        assert(cnt != 4'd10);
    end
endmodule

先看 cover 形式。depth 3 时，搜索窗口只有前 3 拍，离第 11 拍还差得远，smtbmc 逐拍检查可达性后给出 Unreached，sby 以 rc=2 收场：

读这段输出抓三个点。Checking cover reachability in step 0.. 到 step 2.. 是求解器逐拍扩大搜索窗口的过程，每一拍问一次「目标状态在这一拍可达吗」；Unreached cover statement at cover.v:7 给出源码位置，说明工具确实检查到了这条 cover，只是窗口内无解；结尾 engine_0 did not produce any traces 与 DONE (FAIL, rc=2) 要连读——没有产出 witness 轨迹，所以任务判 FAIL。注意这个 FAIL 描述的是「覆盖目标未达成」，不是「设计违反了什么」。

同一个 sby 配置只把 depth 从 3 改成 12，搜索窗口盖住第 11 拍，结论立刻反转：

Reached cover statement ... in step 11. 这行是 cover 任务最想看到的结果：求解器不仅判定可达，还构造出一条 11 拍的 witness 轨迹证明它。CASE A 与 CASE B 的 RTL、引擎、模式完全相同，唯一差异是 depth 一个数值——这正是「cover 的 FAIL 先怀疑 depth 不够」的实测依据。

再看 assert 形式的 bmc。断言 cnt != 10 在这个设计里注定守不住，但 depth 3 的窗口够不到第 11 拍，于是出现一个具有迷惑性的 PASS：

Status: passed 加上 did not produce any traces，翻译过来是「前 3 拍没找到反例」。把 depth 加大到 12，同一条断言立刻被证伪，反例轨迹落盘成 VCD：

CASE C 与 CASE D 并排，就是 bmc 有界性的活教材：depth 3 的 PASS 没有能力对第 4 拍以后的世界做任何承诺。工程上反例常埋在几百拍深的状态机里，depth 给小了会长期收获「绿色的 PASS」，直到调大 depth 或换引擎才爆雷。

二、工具与版本

本次复现的工具链与日志头部记录一致，版本信息直接影响结论口径，不要跨版本照抄：

项	实测值
形式化前端	SBY（SymbiYosys，oss-cad-suite 发行版，配套 yosys 0.43）
SMT 求解器	z3 5.3.3（Python 虚拟环境内 pip 安装的 z3-solver）
引擎配置	smtbmc z3，四组任务仅 mode 与 depth 不同
宿主自带 yosys	apt 版 0.9，不带 smtbmc，无法用于本实验
被测设计	4 位递增计数器，cover 与 assert 两种写法各一份
任务返回码	rc=0 任务通过；rc=2 证伪或覆盖未达成；rc=3 为 unknown（含真超时）

末行的返回码语义值得单独记住。rc=2 在 sby 里是「有确定结论但结论是否定的」——cover 没够着、bmc 抓到反例都归它；真正的求解器墙钟超时（配置里的 timeout 到期、引擎被杀）归 unknown 类、返回码 3，日志里出现的是 timeout 字样而不是 FAIL。把 rc=2 当「超时」去调超时参数，方向从第一步就错了。引擎装不上、smtbmc 找不到求解器的报错是另一条路径，见姊妹篇 sby 引擎与求解器缺失速查。

三、根本原因：depth 语义与两种模式的结论强度

把「看到结论 → 判读 → 调参」的决策链画成流程图，颜色按角色区分：红是界内 FAIL 或反例，蓝是判读动作，橙是调参动作，绿是可达或归纳闭合的强结论。

读这张图抓住两条主线。明线是 depth 的物理意义：smtbmc 把 RTL 综合成 SMT 模型后，从第 0 拍到第 depth 拍逐层展开状态转移关系，depth N 划定的是一个有限长度的展开窗口，求解器在这个窗口内回答「可达吗」「有反例吗」，它是拍数上界，与秒表无关；窗口之外的行为，工具一律不发言。暗线是模式决定结论方向：cover 问「目标能不能到达」，FAIL 是没找着路；bmc 问「断言会不会被违反」，PASS 是没找着反例——两个「没找着」都受同一个窗口约束，把任一个读成全称判断都会误事。

bmc 与归纳证明的强度差，值得再掰开说一层。bmc 的数学口径是「不存在长度不超过 depth 的反例」，depth 再大也是有限值，报告里只能写有界结论；mode prove 在 BMC 之外再加时序归纳（k-induction）：先证明前 k 拍断言成立，再证明「任意连续 k 拍成立能推出下一拍也成立」，归纳步一旦闭合，结论就升级为对任意输入序列、任意运行长度都成立。这个机制在 SVA 断言基础的 sby 实证里有同工具链的 PASSED 实录；归纳的前提是设计状态空间有限且 assume 约束充分，深流水线或约束不全时归纳步可能闭不上，那时 sby 会停在有界结论，不要硬等。

bmc FAIL 落盘的 engine_0/trace.vcd 是求解器构造的最短反例，打开波形逐拍代入断言，先验证反例本身是否合法；若波形里出现协议不允许的输入，病根是 assume 写少了，回去补环境约束而不是改 RTL。

四、排查清单

遇到 sby 的 FAIL、PASS 或疑似「证明超时」，按下面顺序收敛，每一步都有明确判别标准：

步骤	动作	判别
1	读日志结尾返回码与结论词	rc=2 是确定的否定结论，rc=3 含 timeout 才是真超时；先分类再排查
2	打开 .sby 确认 mode	cover 与 bmc 的 FAIL 语义相反，混用解读是第一大误判源
3	手算目标状态最早可达拍数	从复位值沿状态转移推，本例 cnt==10 在第 11 拍；拿不准就先给大 depth 试跑
4	对照 depth 是否覆盖该拍数	cover FAIL 且 depth 小于最早可达拍，确诊为窗口不够，与设计对错无关
5	bmc PASS 时检查结论强度	看报告是否有归纳成功字样；纯 bmc 的 PASS 一律按有界结论引用
6	bmc FAIL 时打开 trace.vcd	逐拍核对反例是否合法，区分「设计真错」与「assume 缺失」
7	确属求解器跑不动再换引擎	日志有 timeout/unknown、单步求解时间异常膨胀才进入引擎切换，换引擎不改变界内结论

两个常见弯路。其一，不要把 depth 当超时旋钮一路加大——depth 翻倍会让展开的 SMT 公式规模显著增长，求解时间往往非线性上涨，正确做法是按最早可达拍数给出略有余量的窗口。其二，cover 任务的 FAIL 不要直接当作缺陷单提出去，先完成第 3、4 步的拍数核算；本篇 CASE A 就是一个纯参数问题，设计本身没有任何错误。

五、修复：调 depth、换 mode、切引擎与复跑确认

第一类修复最直接：depth 给小了就加大到覆盖目标可达拍数。错误配置与修复配置只差一行：

# cov3.sby：窗口只有 3 拍，够不到第 11 拍的目标
[options]
mode cover
depth 3

[engines]
smtbmc z3

[script]
read_verilog -formal cover.v
prep -top top

[files]
cover.v

# cov12.sby：depth 加到 12，覆盖第 11 拍，复跑 Reached
[options]
mode cover
depth 12

[engines]
smtbmc z3

[script]
read_verilog -formal cover.v
prep -top top

[files]
cover.v

第二类修复针对 bmc 有界 PASS 的强度不足：把模式从 bmc 换成 prove，让 smtbmc 在有界检验之后追加时序归纳，归纳闭合拿到的才是任意深度成立的强结论：

[options]
mode prove
depth 20

[engines]
smtbmc z3

[script]
read_verilog -formal reach.v
prep -top top

[files]
reach.v

第三类是引擎切换，适用场景必须卡死：它解决「求解器在合法窗口内跑不动」的墙钟问题，不是本篇的界内 FAIL。RTL 综合后的 SMT 公式大多是位向量逻辑（QF_BV），boolector 在这类公式上通常比 z3 快，yices 在位向量与线性算术混合场景也常有优势；z3 的长处是表达支持全面、行为稳健，适合作为默认引擎。sby 允许在 [engines] 段并列多个引擎并行竞速，先出结论者生效：

[engines]
smtbmc z3
smtbmc boolector
smtbmc yices

复跑确认看两个信号：cover 任务见到 Reached cover statement ... in step N 加 DONE (PASS, rc=0)，且 N 落在你手算的可达拍数附近；prove 任务见到归纳成功的 PASSED 而不是仅 BMC 无反例。若是调引擎的场景，对比两份运行的单步求解时间，确认耗时瓶颈确实转移了再收口。更多形式化模式的方法论背景见 形式化验证基础，接口属性的完整 sby 工程样例见 AXI-Lite 接口的 SVA 形式化检查。

实验环境

• 机器/系统：云主机 / Ubuntu 22.04
• 工具版本：SBY（oss-cad-suite 发行版，配套 yosys 0.43）；z3 5.3.3（Python 虚拟环境内 pip 安装的 z3-solver）；宿主 apt 自带 yosys 0.9 不含 smtbmc，未参与实验
• 日期：2026-11-04
• 完整命令：sby -f cov3.sby cov12.sby bound3.sby bound12.sby（smtbmc z3，四组任务仅 mode 与 depth 不同；实验包内 ./run.sh 依次执行并留存各组日志）

代码获取

四份 sby 配置、cover.v 与 reach.v 两份 RTL、复跑脚本 run.sh 及完整日志已同步到公开仓库：geek-doc.cn/experiments/sby-smtbmc-timeout。备好 oss-cad-suite 与 z3-solver 后执行 ./run.sh，即可按 CASE A 到 D 的顺序重现「cover depth 3 界内 FAIL → depth 12 可达 PASS、bmc depth 3 有界 PASS → depth 12 反例 FAIL」的完整对照。

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

本篇是 EDA 报错排查系列 中形式化工具簇的一员，管的是「工具跑通了、结论读错了」这一层：断言与 sby 基础实操读 SVA 断言基础的 sby 实证，BMC 与归纳证明的原理读 形式化验证基础，完整接口属性工程读 AXI-Lite 接口的 SVA 形式化检查；工具安装层的问题（smtbmc 找不到、求解器缺失）由姊妹篇 sby 引擎与求解器缺失速查 承接，两篇合起来覆盖「环境装不好」与「结论读不对」两大入门卡点。

总结

sby smtbmc 证明超时类困惑的根子是把 depth 当成了超时：depth 是检验拍数的上界，划定的是有限展开窗口，与墙钟时间无关。四组实测显示，cover 的 FAIL(rc=2) 只表示目标在窗口内不可达、不代表恒假，depth 从 3 加到 12 即从 Unreached 变为第 11 拍 Reached；bmc 的 PASS(rc=0) 只是界内无反例的有界结论，同一条断言 depth 12 即被反例证伪并落盘 trace.vcd，要强结论须换 mode prove 走时序归纳。排查按「返回码分类 → 确认 mode → 手算最早可达拍数 → 对照 depth → 区分有界与归纳」推进；只有真超时（unknown、timeout 字样）才进入 z3 到 boolector/yices 的引擎切换，换引擎改变的是求解速度，永远改变不了界内结论。