使用 yices 进行正式验证——管道损坏

编程问答 2022-05-02

问题描述

我正在尝试正式验证我的 verilog FPGA 设计 led_walker.v。所以我首先将其合成为一个 .smt2 文件：

┌───┐
│ $ │ ziga > ziga--workstation > 001--led_walker--verification
└─┬─┘ 
  └─> yosys \
    -p "read_verilog -sv -formal led_walker.v" \
    -p "prep -nordff -top led_walker" \
    -p "write_smt2 led_walker.smt2 "

然后我使用带有 led_walker.smt2 的综合 yosys-smtbmc 文件，使用 BMC 方法来正式验证我的设计：

┌───┐
│ $ │ ziga > ziga--workstation > 001--led_walker--verification
└─┬─┘ 
  └─> yosys-smtbmc led_walker.smt2
##   0:00:00  Solver: yices
Traceback (most recent call last):
  File "/usr/bin/yosys-smtbmc",line 392,in <module>
    smt.write(line)
  File "/usr/share/yosys/smtio.py",line 413,in write
    self.p_write(stmt + "\n",True)
  File "/usr/share/yosys/smtio.py",line 297,in p_write
    if flush: self.p.stdin.flush()
brokenPipeError: [Errno 32] broken pipe

此命令尝试使用求解器 yices 并且看起来它已损坏... 我对形式验证完全陌生，作为一个新手，我不知道这个错误是由于我的设计有缺陷还是系统问题？对我来说，它看起来像一个 python 错误...

这是另一个尝试，但这次我使用 -i 标志指示 yices 使用归纳方法正式验证我的设计。它再次失败（实际上是同样的事情）：

┌───┐
│ $ │ ziga > ziga--workstation > 001--led_walker--verification
└─┬─┘ 
  └─> yosys-smtbmc -i led_walker.smt2
##   0:00:00  Solver: yices
Traceback (most recent call last):
  File "/usr/bin/yosys-smtbmc",line 398,line 430,line 314,in p_write
    if flush: self.p.stdin.flush()
brokenPipeError: [Errno 32] broken pipe

二进制文件 yosys-smtbmc 作为当前版本的官方软件包 yosys 的一部分安装：

┌───┐
│ $ │ ziga > ziga--workstation > ~
└─┬─┘ /dev/pts/10
  └─> yosys -V
Yosys 0.9 (git sha1 1979e0b)

Solver yices (version 2.6.2) 从官方网站 here 下载为预编译二进制文件，使用 install-yices 脚本提取和安装。 >

它们是这样安装的并且对系统可见：

┌───┐
│ $ │ ziga > ziga--workstation > local
└─┬─┘ 
  └─> pwd
/usr/local

┌───┐
│ $ │ ziga > ziga--workstation > local
└─┬─┘ 
  └─> ag -l --search-binary yices
include/yices_exit_codes.h
include/yices_types.h
include/yices_limits.h
include/yices.h
bin/yices-sat
lib/libyices.so.2.6.2
bin/yices-smt
bin/yices-smt2
bin/yices

有谁知道为什么会这样？是否有可能安装 ˙yices˙ 的旧版本会有所帮助？或者也许我缺少一些 python 包？

解决方法

我找到了解决方案。问题在于预编译的二进制文件！如果我从 GitHub 获取最新的开发源然后编译，一切正常。

正确的做法是：

git clone https://github.com/SRI-CSL/yices2.git yices2
cd yices2
autoconf
./configure
make -j$(nproc)
sudo make install

太糟糕了，没有 debian （不是他们提供的 ubuntu PPA 存储库，无法运行） 包！

yicesyosys