[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
Mon Jun 1 18:06:10 BST 2020


--- Comment #30 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Cole Poirier from comment #26)
> (In reply to Luke Kenneth Casson Leighton from comment #25)
> > (In reply to Cole Poirier from comment #24)
> > 
> > > Luke, is the use of Settle() warranted in the synchronous part of this proof?
> > 
> > not at all.
> > 
> > l.
> Thanks, this helps clarify a little bit more for me the use and
> functionality of Settle().
> I think the proof as it stands may need a re-org... I tried filling in the
> quadrants according the to 4-way truth table comment draft that I did, which
> I saw you fixed. But nothing passes but the same Assert you added when you
> fixed the truth table a few days ago (this is actually the else condition in
> the code, but modified here to If for clarity):
> ```
> with m.If(not Past(wp.wen)):
>     # if wen not set, reg should not change
>     comb += Assert(reg == Past(reg))
> ```
> 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,
> or that Regfile itself doesn't properly implement what the proof says it
> should... I'm thinking I should try re-organizing the proof first to see if
> that improves things? What do you think?

I'm taking a look at regfile.py as well as the proof. Part of the reason you
see everything failing is that the truth table in the proof isn't right; the
register file doesn't have a defined output when read enable is low. I have an
idea as to how to prove that register writes work, would you like me to write
it or leave it up to you?

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

More information about the libre-riscv-dev mailing list