[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
Thu May 28 02:18:42 BST 2020


--- Comment #12 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #11)
> (In reply to Cole Poirier from comment #10)
> > Tests now actually run, so I pushed a new commit. In order to formally
> > verify class Register(), I think I've done most of it, but there's a part of
> > the class's elaborate function that uses sync instead of comb, and I'm not
> > sure how to do this in proof form.
> one way is to use Past()

Sorry for the delay. I did a git pull and added an Assert using Past() but my
proof is still failing. I pushed my commit. Can you take a look when you can to
help me identify where I've erred?

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

More information about the libre-riscv-dev mailing list