[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=316

--- Comment #32 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #31)
> try running a different formal test that is known to already work.

Unfortunately, after several hours and multiple re-installations of nmigen,
nmutil, ieee754fpu, soc, yosys, symbiyosys, and dist-packages cleanings, when
trying to run known working proof '~/src/soc/src/soc/decoder/formal$ python3.7
proof_decoder.py'
I get the same error with the following output:
```
mask 0x1f
E
======================================================================
ERROR: test_decoder (__main__.DecoderTestCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "proof_decoder.py", line 125, in test_decoder
    self.assertFormal(module, mode="bmc", depth=4)
  File "/home/colepoirier/src/nmigen/nmigen/test/utils.py", line 100, in
assertFormal
    stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc:
  File "/usr/lib/python3.7/subprocess.py", line 775, in __init__
    restore_signals, start_new_session)
  File "/usr/lib/python3.7/subprocess.py", line 1522, in _execute_child
    raise child_exception_type(errno_num, err_msg, err_filename)
FileNotFoundError: [Errno 2] No such file or directory: '': ''

----------------------------------------------------------------------
Ran 1 test in 3.459s

FAILED (errors=1)
```

-- 
You are receiving this mail because:
You are on the CC list for the bug.