用yices进行的正式验证.断裂的管道

Question

我试图正式验证我的verilog设计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，它看起来好像坏了.我对正式验证完全陌生，作为一个新手，我不知道这个错误是由于我有缺陷的设计还是系统问题？在我看来就像是蟒蛇的错误..。

这里是另一次尝试，但这次我使用了-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 (Version2.6.2)是从官方网站这里下载的预编译二进制文件，使用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·将有所帮助？还是梅比我漏掉了一些蟒蛇包？

Answer 1

我找到了解决办法。问题在于预编译的二进制文件！如果我从GitHub获得最新的开发源，然后编译，那么一切都能正常工作。

这就是如何正确地做这件事：

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

可惜没有debian (不是他们提供的bad存储库)包！