[libre-riscv-dev] [Bug 335] Formal Correctness Proof for Branch pipeline

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sun May 24 20:20:03 BST 2020


--- Comment #10 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #9)
> hm i feel the need to assert that when the cases are not being enabled,
> the registers not in use (not changed) should be Asserted 0
> (self.o.{something}.ok == 0)
> this because if they are not zero they will cause a request for a
> register port write at the MultiCompUnit, which, because their data
> (self.o.{something}.data) was not initialised, would cause regfile
> corruption.

Good idea - done. Caught a bug where a regular branch would write to ctr if the
branch immediate was just right (or wrong).

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

More information about the libre-riscv-dev mailing list