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