[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
Sat May 30 23:38:42 BST 2020


--- Comment #27 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cole Poirier from comment #26)

> This leads me to believe that either the proof is wrong and needs to be
> reorganized to conform to how Register is implemented in regfile/regfile.py,

the unit test for RegFileArray and RegFile leads me to believe that it is.
however it is worthwhile confirming this by writing a straight unit test,
exactly is done in regfile.py.

basically i have no idea what i am doing with Formal Proofs.  i can read
them, i can *maybe* spot omissions once they're written, and i can just about
manage combinatorial ones.  these sync/time-based ones: really no idea.

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

More information about the libre-riscv-dev mailing list