极客工场

Appearance

共 2,310 字预计阅读约 8 分钟

Yosys 形式验证 smtbmc 失败：报错与反例定位速查 ​

更新时间：2026-10-25。FAQ 速查页，属于 FPGA 开源工具链排错系列。用 Yosys 做形式验证，yosys-smtbmc 要么直接报错退出、要么给出一个你不相信的反例（counterexample）——这两类「失败」性质完全不同：一个是工具链没搭好，一个是证明真的没成立（或你的约束写错了）。本文以 smtbmc 的真实输出为锚逐条分诊。Yosys 综合侧的报错见 Yosys module not declared，开源工具链全景见 FPGA 开源工具链。

本文要回答的问题 ​

  • smtbmc: error: solver not found 之类报错怎么解？
  • z3、yices、boolector 该选哪个，-s 参数怎么给？
  • 反例（SAT 结果）给出的 VCD 怎么读、怎么定位到信号？
  • assume 写多了为什么会「假通过」（vacuous）？
  • BMC 深度不够时，k-induction 怎么接力？

一、报错原文与现象 ​

text
smtbmc: error: no SMT solver available (tried: z3, yices, boolector)
text
##  Status: SAT (assertion failed)
##  found counterexample, writing to counterexample.vcd

第一种是求解器缺失：smtbmc 自己不做求解，它把问题翻译成 SMT-LIB 格式交给外部求解器，一个都找不到就直接退出。第二种是「找到了反例」——这在语义上是工具正常工作、断言被推翻了；你的任务是读懂反例，判断是设计真错还是约束写错。第三种常见现象是 Status: UNKNOWN，即求解器在给定深度内给不出结论，多半要调深度或换求解器。

二、可能原因总览 ​

报错/现象可能原因处置
no SMT solver availablez3/yices/boolector 都没装包管理器装 z3 起步
求解器装仍报找不到二进制不在 PATHwhich 确认，补 PATH
Status: SAT 意外反例约束写错或设计真错读反例 VCD 定位信号
反例里信号全 Xwitness 初态未约束复位序列或 initial 约束
证明永远 UNKNOWN深度不够或求解器吃力加深度、换 -s 选型
断言明显该过却 SATassume 覆盖了时钟/复位检查 assume 集合冲突
全 PASS 但不可信assume 过强导致 vacuous加 cover 语句验证可达性
挂死无输出求解器陷入难分岔缩深度、简化设计

三、逐条排查展开 ​

求解器缺失是第一条分水岭。 smtbmc 支持 z3、yices、boolector、mathsat 等求解器，-s 参数指定用哪个。最小可用配置是装一个 z3：

bash
# Debian/Ubuntu
sudo apt install z3
# 确认
which z3 && z3 --version
yosys-smtbmc -s z3 -t 20 design.smt2

which 找不到就是没装或不在 PATH；装好再跑。工程上建议至少备两个求解器（z3 + yices），同一个证明换求解器经常从 UNKNOWN 变成可判——不同求解器在不同结构上强弱互补。

反例 VCD 的读法有固定套路。 SAT 结果写出的 VCD 是「让断言失败的那一具体执行轨迹」，加载进 GTKWave 后按三步读：先看失败的 assert 对应信号在哪一拍变假；再沿该信号的数据依赖往回追到输入或状态寄存器；最后检查这个轨迹是否经过了「你认为不可能发生」的状态组合——如果是，说明你漏了 assume；如果轨迹完全合法，那设计就是真错。常见的「假反例」来源是初态：BMC 从任意初态出发，没有复位约束时，寄存器可以取到正常运行永远到不了的值，断言自然被打翻。处置：在 testbench 里约束复位序列（前几拍复位有效），或用 Yosys 的 formal 模式配合 initial 块给状态一个合法起点。

assume 与 assert 是天平两端。 assume 太弱 → 假反例泛滥（上一种情况）；assume 太强 → 反例空间被压空，所有断言「通过」但证明是空集上成立的（vacuous pass），什么也说明不了。检测方法：给关键场景加 cover 语句——

systemverilog
cover property (@(posedge clk) req ##1 ack);

cover 能找到一条满足轨迹，说明 assume 约束下该场景仍可达；cover 全是 UNREACHABLE，说明 assume 已经把设计行为压没了，断言的 PASS 不可信。assume 集合冲突（两条 assume 合起来矛盾）同样导致全部 vacuous，逐条注释排查能定位。

深度不是越大越好，是要「够」。 -t N 指定 BMC 展开 N 拍。断言涉及的最长时序窗口是 4 拍，你给深度 8 才有完整结论；深度小于窗口时，smtbmc 报告的是「在 N 拍内没找到反例」，这不是证明通过。判断深度是否够：看断言里最长的 ##[a:b] 上界、流水线级数、状态机最长路径，取最大值再加余量。深度给足仍 UNKNOWN 的，进入下一步。

k-induction 是有界证明通向无界证明的桥。 BMC 只能证「前 N 拍无反例」，k-induction（smtbmc 的 -i 相关流程或 SymbiYosys 的 prove 模式）试图证「任意拍都成立」：基例用 BMC 查前 k 拍，归纳步假设任意 k 拍成立证第 k+1 拍。归纳失败通常需要给设计补归纳引理（invariant）——把一些「任何时刻都成立」的性质写成额外 assert 帮助归纳收敛。SymbiYosys（sby）把整套流程（BMC + induction + 多引擎）打包好，手写 smtbmc 命令排不动时，迁到 sby 配置管理是省时方向：一份 .sby 文件声明文件清单、深度、引擎列表，sby -f design.sby 一条命令跑完并给出带状态的报告目录，失败时的反例与日志自动归档，回归接入也只需一行命令。

smtbmc 的诊断选项能省一半猜测。 加 --dump-smtc 把生成的 SMT 约束落盘，可以在求解器外手工检查约束内容是否符合预期；加 verbose 相关选项能看到每一拍的展开与求解耗时——某一拍耗时陡增说明状态空间在那里爆炸，提示你在那一带加 assume 约束或简化逻辑。反例 VCD 之外，smtbmc 还会在终端打印失败断言的名字与拍号，先读终端再开 GTKWave，方向明确得多。

最小复现是求助与自救的利器。 把失败设计裁到只剩相关模块与断言（yosys -p 'read_verilog -formal min.sv; prep -top min' 产出的 smt2 几十行），一半以上的「工具问题」在裁剪过程中会自己现形——剩下的才值得深究。

四、排查流程图 ​

这张图按「先工具链、再读反例、后调证明强度」组织分诊。红色是故障/根因类节点，蓝色是排查动作，绿色是证明通过的确认，橙色是修复动作，紫色是流程沉淀。

fpga/ts-yosys-formal-smtbmc-fail.md D2 示意图

读这张图注意主干顺序：求解器问题三十秒排除，反例判读是主要工作量所在，加深度与归纳只在「轨迹合法、深度给足」之后才登场——不要一上来就和 k-induction 搏斗。

五、预防与纪律 ​

  • 求解器双备份：z3 + yices 常驻环境，UNKNOWN 时先换引擎再改设计。
  • 复位约束是默认动作：所有 formal testbench 开头约束复位序列，初态假反例从源头消灭。
  • 关键场景配 cover：每组断言带可达性 cover，vacuous pass 能被回归自动发现。
  • 深度写注释：-t 的取值依据（最长时序窗口）写在脚本注释里，改设计时同步复核。
  • 迁移到 SymbiYosys：超过两条断言的模块用 sby 管理，BMC/induction/多引擎一份配置。
  • 反例 VCD 归档：真错的反例随 bug 单归档，复盘时可直接重放轨迹。

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

本篇是开源工具链排错簇中「形式验证」节点的 FAQ 页：与 Yosys module not declared（综合侧）、Yosys 连接被拒（环境侧）、Verilator 排错簇（仿真侧）互补；开源工具链入门见 FPGA 开源工具链，断言写法基础见 SystemVerilog 可综合子集，系列总览见 FPGA 知识版图。

一句话总结 ​

Yosys smtbmc 失败分三层处理：工具链层确认 z3 等求解器装好且在 PATH、-s 选型明确；反例层用 VCD 三步读法区分假反例（初态未约束、assume 过弱）与真错，assume 过强导致的 vacuous pass 用 cover 可达性兜底检测；证明强度层把 -t 深度给到覆盖最长时序窗口，仍 UNKNOWN 就换求解器或上 k-induction/SymbiYosys 补不变量引理，最后把求解器双备份、复位约束、cover 回归固化成形式验证的默认模板。