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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Michael Nolan from comment #4)

> Ah, it looks like power_decoder2 already handles this for us. It only sets
> dec2.e.lk if the instruction has the lk flag set in the table, and LK is set
> in the instruction field.

yyeah i think that was me, doing something random (which i now don't
quite follow, but i did at the time).  this should be commented.

also it occurs to me that similar things need to be done to check that
{insert_data_thing}.ok == 0 at appropriate points, because the plan is to 
actually use those in the CompUnits, to set the "REQUEST_WRITE" flags.

if for example ctr.ok is set to 1 when it should not be, the CTR SPR
would get corrupted data sent to the register file.

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