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

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=335

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #10)
> (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).

these are not fully showing up because we do not have writes to regfile(s) yet.
 if we put together the regfiles and a quick link to the pipelines through the
CompUnits interface, we pretty much have a working CPU done and can catch these
things, because SPRs,  XER, etc will all be spuriously modified.

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