[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