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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon May 18 01:45:53 BST 2020


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

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_", "")

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.

More information about the libre-riscv-dev mailing list