yosys

Formal verification with yices -- broken pipe

I am trying to formally verify my verilog FPGA design led_walker.v. So I first synthesize it to an .smt2 file:

┌───┐
│ $ │ 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 "

I then use synthesized led_walker.smt2 file with yosys-smtbmc to formally verify my design using BMC method:

┌───┐
│ $ │ 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

This command tries to use a solver yices and it looks like it is broken... I am completely new to formal verification and as a newcommer I don't know if this error is due to my flawed design or is this a system problem? To me it looks like a python error...

Here is another try but this time I use -i flag that instructs yices to formally verify my design using induction method. It fails again (same thing actually):

┌───┐
│ $ │ 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

Binary yosys-smtbmc was installed as part of the official package yosys that is currently version:

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

Solver yices (version 2.6.2) was downloaded as precompiled binaries from official website here, extracted and installed using the install-yices script.

They are installed like this and visible to the system:

┌───┐
│ $ │ 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

Does anyone have any idea why this is happening? Is there any possibility that installing older versions of the ˙yices˙ would help? Or maybee I am missing some python packages?

Solution

  • I found a solution. Problem is with the precompiled binaries! If I get the latest development sources from the GitHub and then compile, everything works.

    This is how to properly do it:

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

    Too bad that there is no debian (not ubuntu PPA repository that they provide and is not working) package!