[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: Thu, 28 May 2020 01:33:08 +0000
Message-ID: <bug-353-13-tT0dQGCuxY@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 #13 from Luke Kenneth Casson Leighton <lkcl@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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev