用 yices 进行形式化验证 -- broken pipe

Question

我正在尝试正式验证我的 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 "

然后我使用带有 yosys-smtbmc 的合成 led_walker.smt2 文件，使用 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, in <module>
    smt.write(line)
  File "/usr/share/yosys/smtio.py", line 430, in write
    self.p_write(stmt + "\n", True)
  File "/usr/share/yosys/smtio.py", 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 （版本 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 包？

Answer 1

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

这是正确的做法：

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

太糟糕了，没有 debian （他们提供的不是 ubuntu PPA 存储库，但无法正常工作） 软件包！

用 yices 进行形式化验证 -- broken pipe

Formal verification with yices -- broken pipe

yosys