[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 22:41:08 BST 2020


--- Comment #24 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Cole Poirier from comment #23)
> (In reply to Luke Kenneth Casson Leighton from comment #22)
> > done.  updated.  basically, this is... complicated.  there's time-dependent
> > interactions.  i actually managed to get one case to work: when wen is
> > not set, the reg should not change.  past value should equal the present
> > value.
> Ah it's time-dependent, that makes sense. Thanks, pulled and ran the test.
> Cool. How would I go about better understanding how ren and wen are supposed
> to interact? Studying the logic diagram? Or something else?

Luke, is the use of Settle() warranted in the synchronous part of this proof?

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

More information about the libre-riscv-dev mailing list