[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 #13 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
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.

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