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