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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #30 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Cole Poirier from comment #29)
> 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)
> ```

Nope, no arguments needed. I ran into this error a while ago, it's something to
do with symbiyosys not finding a file. I'm not sure how it got fixed though, as
it seemed to resolve itself. Are you using the latest nmigen, installed from
the git repo?

-- 
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