[Libre-soc-bugs] [Bug 421] TRAP pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
ok so i read the spec here a bit more closely, and the msr_copy
function is being used to copy a range of bits from SRR1 to MSR,
which, if, following that, some bits of SRR1/MSR were set, then
some bits in MSR need to be *restored* i.e. the original (msr_i)
needs to overwrite those bits, instead.

i think the best thing to suggest, here, sam, is for the formal
proof to do what the *pseudocode* does, *not* what trap main_stage.py
does.

however i think what i am going to have to do is to alter the
pseudo-code and write to the openpower-hdl-cores list (again)
to notify them of a discrepancy in the pseudo-code.

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