使用yices做Verilog形式验证时yosys-smtbmc触发BrokenPipeError求助

错误成因 #

这个BrokenPipeError是yices求解器进程被提前终止导致的，和你的Verilog设计、Python依赖包都没有关系，核心原因是版本兼容性问题：
你当前使用的Yosys 0.9属于2020年发布的旧稳定版本，只适配yices 2.6.0及更早的版本，你安装的yices 2.6.2更新了SMT命令解析逻辑，旧版yosys-smtbmc传递的SMT指令无法被新版yices识别，导致yices进程启动后直接崩溃退出，yosys-smtbmc往已经关闭的yices进程标准输入写数据时就会触发管道断裂报错。

相关问题解答 #

• 是否是缺失Python依赖包导致的？
  不是。报错堆栈指向子进程标准输入写入失败，说明故障出在被调用的yices进程侧，不是Python运行环境缺少依赖。
• 安装更低版本的yices是否可以解决该问题？
  可以。安装yices 2.6.0或者2.5.x版本即可和Yosys 0.9正常适配，是成本最低的解决方案。

其他可选解决方案 #

如果不想降级yices，也可以选择以下两种方案修复问题：

• 更换求解器：调用时指定使用z3求解器，不需要修改现有环境配置，执行命令如下：

  yosys-smtbmc -s z3 led_walker.smt2
  

  如系统未安装z3，直接通过系统包管理器安装即可，例如Debian/Ubuntu系执行apt install z3。
• 升级Yosys：将Yosys升级到最新稳定版本，新版Yosys已经修复了对高版本yices的兼容问题，适配yices 2.6.x系列所有版本。

内容的提问来源于stack exchange，提问作者71GA