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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon May 18 00:44:25 BST 2020


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

--- Comment #33 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
Cole, one critically important thing that you need to learn as a "first
reaction"
is to go through every single file, at every single line, on a stack trace,
actually seeing what that line (and nearby) actually does.

here is the relevant line of nmigen.test.utils:

        with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name],
cwd=spec_dir,
                              universal_newlines=True,
                              stdin=subprocess.PIPE, stdout=subprocess.PIPE) as
proc:
            stdout, stderr = proc.communicate(config)

also, that it is perfectly find to insert debug print statements into that
code in order to find out what is going on.

for example, do this:

        sbytool = require_tool("sby")
        print ("sby tool blah blah", sbytool, spec_name, spec_dir)
        with subprocess.Popen([sbytool, "-f", "-d", spec_name], ....


then, if that is not obvious what is going on, drill down into require_tool,
which can be found in nmigen/_toolchain.py

and there, start dropping in a ton of print debug statements that tell you
what is going on.

print ("env_var", env_var)
print path
print shutil.which(path)
print os.environ.keys()

etc blah blah blah

further up the assertFormal function, start dropping in print statements there.

basically, when you've done all that, try this:

lkcl at fizzy:~/src/libresoc/soc/src/soc/logical/formal$ python3 proof_bperm.py

and:

lkcl at fizzy:~/src/libresoc/soc/src/soc/logical/formal$ cd ..
lkcl at fizzy:~/src/libresoc/soc/src/soc/logical$ python3 logical/proof_bperm.py

and tell me what happens in each case.

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


More information about the libre-riscv-dev mailing list