[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed
bugzilla-daemon at libre-soc.org
bugzilla-daemon at libre-soc.org
Mon Jun 1 18:51:28 BST 2020
https://bugs.libre-soc.org/show_bug.cgi?id=353
--- Comment #31 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Michael Nolan from comment #30)
> I'm taking a look at regfile.py as well as the proof. Part of the reason you
> see everything failing is that the truth table in the proof isn't right; the
> register file doesn't have a defined output when read enable is low. I have
> an idea as to how to prove that register writes work, would you like me to
> write it or leave it up to you?
Actually, it turned out that the register file wasn't generating read and write
ports.
--
You are receiving this mail because:
You are on the CC list for the bug.
More information about the libre-riscv-dev
mailing list