[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon at libre-soc.org]

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

--- 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.