极客工场

Appearance

共 2,908 字预计阅读约 10 分钟

sby 求解器缺失报错速查：z3 not found 与 hierarchy -smtcheck 语法错的两类签名 ​

更新时间：2026-11-05。报错排查篇，属于 EDA 报错排查系列。SymbiYosys（sby）跑 smtbmc 引擎时的失败，新手最容易把两笔不同的账算成一笔：一笔是 yosys 版本太旧、根本不带 smtbmc 流程，另一笔是 yosys 与 sby 版本配套、但 PATH 上找不到 z3/yices/boolector 求解器二进制。两者的报错签名完全不同，修法也一个在工具链、一个在求解器。sby 的基本用法与 .sby 配置结构见 SVA 断言基础：SymbiYosys 形式化实证。

首屏答案：先看报错落点。base: ERROR: Command syntax error 且光标指在 hierarchy -smtcheck 上，是新版 sby 生成的脚本喂给了旧版 yosys（如 apt 的 yosys 0.9），要换带 smtbmc pass 的新工具链；能看到 ## Solver: z3 紧接着 SMT Solver 'z3' not found in path.，说明 yosys 这层没问题，纯粹是 PATH 上缺求解器，pip install z3-solver 或系统包装好 z3、把其 bin 目录放到 sby 进程的 PATH 前面即可。

sby 求解器缺失报错一张卡：两个签名、两层配套、两条修复路径

这张卡把本篇的主线一次摊开：sby 的一次形式化运行要穿过两道门，先是 sby 调 yosys 综合出 SMT 模型，再是 yosys-smtbmc 调外部求解器求解。两道门各有各的缺件方式，红色两区是报错现场，蓝色区管版本对拍，绿色区管 PATH 对拍，后面三节按这个顺序展开。

本文要回答的问题 ​

  • hierarchy -smtcheck 报 Command syntax error，为什么说这不是 .sby 文件写错了？
  • SMT Solver 'z3' not found in path. 出现时 yosys 到底有没有正常工作？
  • 同一个 smtbmc z3 引擎，yosys 版本问题和求解器问题怎么在三十秒内区分？
  • z3、yices、boolector 三个求解器分别怎么装？装完为什么还要管 PATH 顺序？
  • 修复后复跑，log 里出现什么才算真正修好？

一、报错原文与现象：两个签名，两个失败阶段 ​

复现实验用一个 11 行的最小设计：两个 4 位寄存器在每个时钟沿同步加一，并断言它们始终相等。.sby 文件只有一个引擎 smtbmc z3，在三种 PATH 配置下各跑一次，分别打出两类失败签名和一次修复后的成功运行。先看签名 A——把 PATH 限定为系统目录，让 sby 找到 apt 安装的 yosys 0.9：

CASE A：yosys 0.9 不认 hierarchy -smtcheck，base 阶段即中止

读这张终端卡抓三个要点。第一，失败点在 base 阶段，sby 刚启动 yosys -ql ../model/design.log ../model/design.ys 就挂了，engine_0 (smtbmc z3) did not return a status 说明求解器引擎压根没被拉起来。第二，报错光标精确指在 hierarchy -smtcheck 的 -smtcheck 选项下方，这是新版 sby 生成的综合脚本，而系统里的 yosys 0.9 还没有这个选项，于是按「未知选项」抛出语法错。第三，整条输出里没有任何 Solver: 字样——问题在求解器之前，重装 z3 救不了这个场景。sby 如何生成这段综合脚本，可以对照 SVA 断言基础 里的完整跑通过程。

换成带 smtbmc pass 的 yosys 0.43（oss-cad-suite 工具链），但故意把 z3 二进制挪走，签名立刻变了：

CASE B：yosys 0.43 配套但 PATH 无 z3，引擎阶段 rc=16 退出

这张卡与上一张的差别就是分诊的关键。第一，base 阶段顺利通过，yosys 已经把设计综合成 model/design_smt2.smt2，进程命令行里能看到 yosys-smtbmc -s z3 ... 被正常拉起——版本配套这层是好的。第二，basecase 与 induction 两个进程都先打印 ## Solver: z3，紧接着才报 SMT Solver 'z3' not found in path.，说明 yosys-smtbmc 读完了模型、按 -s z3 的要求去找 z3 可执行文件，扑了空。第三，sby 收尾报 Engine terminated without status 并以 rc=16 结束，引擎没产出任何反例波形文件。看到 Solver: 这一行，就可以把「yosys 版本」从嫌疑名单里划掉。

二、工具与版本 ​

三场景共用同一份 RTL 与 .sby，唯一变量是 PATH 上露出哪套工具，版本全部照实验记录头部抄录：

项实测值
sby / yosys（失败签名 A）系统 apt yosys 0.9，无 smtbmc pass
sby / yosys（签名 B 与修复）oss-cad-suite，yosys 0.43，含 yosys-smtbmc
求解器（修复后）z3 5.3.3，由 pip 的 z3-solver 包装入独立虚拟环境
引擎配置[engines] 段单行 smtbmc z3，mode prove，深度 20
失败退出码签名 B 为 rc=16（引擎无状态退出）；签名 A 在 base 阶段 returncode=1

版本信息在这个主题里不是背景板，而是判据本身。sby 与 yosys 是同仓库姊妹工程，新版 sby 生成的 design.ys 会使用只有新版 yosys 才认识的选项，二者错配就会出现签名 A；而 yosys-smtbmc 与求解器之间是松耦合的运行期调用，它不检查 z3 是哪个发行版装的，只认 PATH 上能不能 exec 到。形式验证工具链的整体分工见 形式验证入门。

三、根本原因：一道门各管一段的两层配套 ​

把三场景的因果画成一张分诊流程图，颜色按角色分：红是两类报错根因，蓝是版本与 PATH 的排查动作，橙是对应的安装修复动作，绿是复跑通过态。

eda/ts-sby-engine-solver-missing.md D2 示意图

读这张图抓住一条主线：先看失败在哪个阶段，再决定动哪一层。base 阶段是 sby 调 yosys 跑综合脚本，挂在这里属于第一层配套断裂——sby 与 yosys 版本错配，任何求解器都没机会上场；engine 阶段是 yosys-smtbmc 拿着综合好的 SMT2 模型调求解器，挂在这里属于第二层配套断裂——模型已经就绪，只差一个能被 PATH 找到的求解器进程。

第二层还有一个隐蔽点：yosys-smtbmc 找的是 sby 进程继承下来的 PATH，不是你交互 shell 里的 PATH。用 sudo、cron、容器 entrypoint 或 IDE 任务起 sby 时，PATH 常常被换成精简版，明明终端里 z3 --version 好好的，sby 子进程却找不到——CASE B 正是用精简 PATH 复现了这个情形。同理，把 z3 装在某个虚拟环境里却不激活它，效果与没装相同。真实工程里用 sby 检查 AXI 握手断言的完整跑通案例见 SVA 检查 AXI 握手，那条链路对 PATH 的要求与本篇完全一致。

四、排查清单：四条命令对拍两层配套 ​

遇到 smtbmc 引擎失败，按下面顺序收敛，每条命令都在回答一个是非题：

步骤命令判定
1看 log 失败落点base 阶段挂走步骤 2；engine 阶段、有 Solver: 行直接走步骤 4
2yosys -V0.9 等老版本基本可断定无 smtbmc pass，需要换工具链
3which yosys yosys-smtbmc确认 sby 实际调到的是不是新版那套，防止新旧并存时 PATH 顺序误导
4which z3 && z3 --version无输出即求解器缺失；有输出还要确认该目录在 sby 进程的 PATH 内
5echo $PATH对照求解器 bin 目录位置，虚拟环境或 oss-cad-suite 的 bin 必须排在前面

两个常见弯路。其一，不要看到 smtbmc z3 就只盯着 z3 重装——签名 A 的场景里 z3 装得再正确，base 阶段也到不了调用求解器那一步。其二，pip install z3-solver 装的是带 Python 绑定的完整 z3，可执行文件落在所在环境的 bin 目录下；只装 Python 绑定而该 bin 目录不进 PATH，yosys-smtbmc 照样找不到，因为它要 exec 的是 z3 命令而不是 import 一个库。

三个求解器与 .sby 引擎名的对应关系也要记牢：smtbmc z3 找 z3，smtbmc yices 找 yices-smt2，smtbmc boolector 找 boolector，缺什么装什么、换引擎名就要换对应二进制，不存在装一个 z3 通吃三种引擎名的写法。

五、修复代码与复跑确认 ​

修第二层配套（签名 B）只需两步。先把 z3 装进一个独立 Python 环境，再让该环境的 bin 目录在 PATH 中优先于其他目录：

bash
sudo /opt/eda-venv/bin/pip install z3-solver
export PATH=/opt/eda-venv/bin:$PATH
which z3 && z3 --version

若是第一层配套断裂（签名 A），动作是替换 yosys 而不是装求解器。以 oss-cad-suite 为例，解压后把它的 bin 目录前置，再用版本命令确认生效：

bash
export PATH=$HOME/oss-cad-suite/bin:$PATH
yosys -V
which yosys-smtbmc

实验用的最小工程配置如下，引擎名与修复动作的对应可以直接在这四行上验证：

ini
[options]
mode prove

[engines]
smtbmc z3

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

[files]
tiny.v

修复后用「虚拟环境 bin + oss-cad-suite bin」的组合 PATH 复跑同一份工程，basecase 与 induction 双双进入正常求解节奏，下面是复跑记录的原样摘录：

exp-log
SBY  2:21:23 [tiny] engine_0: smtbmc z3
SBY  2:21:23 [tiny] engine_0.induction: ##   0:00:00  Solver: z3
SBY  2:21:23 [tiny] engine_0.basecase: ##   0:00:00  Solver: z3
SBY  2:21:23 [tiny] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY  2:21:23 [tiny] engine_0.induction: ##   0:00:00  Trying induction in step 20..
SBY  2:21:23 [tiny] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY  2:21:23 [tiny] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY  2:21:23 [tiny] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..

过关信号有两个：一是 Solver: z3 之后不再出现 not found in path，二是 basecase 持续打印 Checking assertions in step N.. 并逐拍推进、induction 进入 Trying induction，本次运行最终以 PASS（rc=0）收尾。与 CASE B 对照，两次运行的 yosys、RTL、.sby 完全相同，唯一差异就是 PATH 前面多了那个含 z3 的 bin 目录。想换求解器时，把 z3-solver 换成系统包里的 yices 或 boolector，并同步改 .sby 的引擎名即可。

实验环境 ​

  • 机器/系统：Linux 主机 / Ubuntu 系发行版（宿主直接运行，无容器）
  • 工具版本：oss-cad-suite 版 yosys 0.43（含 yosys-smtbmc）；对照用系统 apt yosys 0.9（无 smtbmc pass）；求解器 z3 5.3.3（pip 的 z3-solver，装在独立虚拟环境）
  • 日期：2026-11-04
  • 完整命令：PATH=/usr/local/bin:/usr/bin:/bin sby -f tiny.sby（CASE A，复现版本不配套）；PATH=oss-cad-suite/bin:/usr/bin:/bin sby -f tiny.sby（CASE B，复现求解器缺失）；sudo /opt/eda-venv/bin/pip install z3-solver 后 PATH=/opt/eda-venv/bin:oss-cad-suite/bin:... sby -f tiny.sby（CASE C，修复复跑）

代码获取 ​

最小复现工程（11 行 RTL、四行引擎配置的 tiny.sby、三场景 PATH 切换脚本 run.sh）在公开仓 https://github.com/derekzhuo/geek-doc.cn/tree/main/experiments/sby-engine-solver-missing。按目录内 README 准备一套带 smtbmc 的 yosys 与一个不含 z3 的初始 PATH，执行 ./run.sh 即可重现「语法错失败 → not found 失败 → 装 z3 后 PASS」的完整对照。

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

本篇是 EDA 报错排查系列 中形式验证工具链簇的一员，管的是 sby 跑 smtbmc 引擎时「环境缺件」这一层：工具用法与一次完整的 FAIL/PASS 形式化实证见 SVA 断言基础：SymbiYosys 形式化实证，断言在真实总线上的实战见 SVA 检查 AXI 握手，assert/assume/cover 与有界证明的方法论见 形式验证入门。读这一篇的正确姿势是把它当作那三篇的「环境前置排查」：工具链与求解器就绪之后，断言本身的写法与验证策略才是主角。

总结 ​

sby 求解器缺失报错要按失败阶段拆成两笔账：base 阶段 hierarchy -smtcheck 报 Command syntax error 是 sby 与旧版 yosys（如 0.9）版本不配套，解法是换带 smtbmc pass 的新工具链；engine 阶段先打印 Solver: z3 再报 SMT Solver 'z3' not found in path.（rc=16）是 PATH 上缺求解器，解法是 pip install z3-solver 或系统包安装 z3/yices/boolector，并把对应 bin 目录前置到 sby 进程继承的 PATH；复跑到 Checking assertions in step N.. 连续推进、运行 PASS 收尾即告修复。