[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 #15 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Cole Poirier from comment #14)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > no idea.
> > 
> > first thing though: it is unsafe to mix python parameters that change the
> > entire behaviour of the module.
> > 
> > i suggest starting with two utterly different proofs, divided and isolated
> > with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> > AST.A
> > 
> > then, to do a 4 way (dual nested) set of m.If on ren and wen.
> > 
> > then, in EACH quadrant, do completely separate assertions.
> > 
> > but before making those assertions, write out in words the expected
> > behaviour when the 4 way truth table of wen and ren occurs.
> 
> Ah yes that makes sense. That is how the module I'm trying to verify is
> written after all. Thanks for your guidance and helpful redirection on this.
> I'll work through the 4 way truth table with expected behavior in words then
> report back.

Spent an hour trying to sense of this but I think my brain has given up for the
day. Will make a fresh effort tomorrow.

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