[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 #14 from Cole Poirier <colepoirier at gmail.com> ---
(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.

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