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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #29 from Cole Poirier <colepoirier@gmail.com> ---
Hi Michael, is there an argument that needs to be passed in order to run the
formal proof, or a config.sby file? I'm currently trying 'python3
proof_bperm.py' which gives me an error about a missing file... I'm pulling my
hair out trying to figure out which file it's looking for.

```
E.
======================================================================
ERROR: test_formal (__main__.TestCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "proof_bperm.py", line 112, in test_formal
    self.assertFormal(module, mode="bmc", depth=2)
  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 2 tests in 0.479s

FAILED (errors=1)
```

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev