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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #35 from Cole Poirier <colepoirier at gmail.com> ---
Thank you for the guidance to do standard python debugging, found the bug and
fixed it in minutes.

The key turned out to be adding os.realpath() at the top of the assertFormal()
function:

```
def assertFormal(self, spec, mode="bmc", depth=1):
    caller, *_ = traceback.extract_stack(limit=2)
    spec_root, _ = os.path.splitext(caller.filename)
-   spec_dir = os.path.dirname(spec_root) 
+   spec_dir = os.path.dirname(os.path.realpath(spec_root))
    spec_name = "{}_{}".format(
        os.path.basename(spec_root).replace("test_", "spec_"),
        caller.name.replace("test_", "")
    )
    [snip..]
```

Should I make a PR to nmigen with this fix?

I'm stopping work for today. Will pick this up and make my 'real' first proof
attempt in the morning.

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