[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed - bugzilla-daemon

From: bugzilla-daemon@libre-soc.org
To: libre-riscv-dev@lists.libre-riscv.org
Subject: [libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed
Date: Mon, 01 Jun 2020 17:06:10 +0000
Message-ID: <bug-353-13-sa7KetKSEs@https.bugs.libre-soc.org/> (raw)
In-Reply-To: <bug-353-13@https.bugs.libre-soc.org/>

https://bugs.libre-soc.org/show_bug.cgi?id=353

--- Comment #30 from Michael Nolan <mtnolan2640@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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev