[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 23:13:17 BST 2020


--- Comment #26 from Cole Poirier <colepoirier at gmail.com> ---
(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?

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

More information about the libre-riscv-dev mailing list