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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Thu May 28 02:33:08 BST 2020


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

More information about the libre-riscv-dev mailing list