[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 #11 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)
>     If MSR3=1 then bits 3 and 51 of SRR1 are placed into
>     the corresponding bits of the MSR.
> 
> do those look consistent to you? (nobody has really properly
> reviewed the pseudocode in the spec so inconsistencies are
> expected)

In this particular case, yes; but it requires some thought to see it.

If MSR[3]=1, then MSR[3] and MSR[51] are overwritten.

If MSR[3]=0, then MSR[3] and MSR[51] are to remain stable.  But, since MSR[3]
is already 0, the logical AND of MSR[3] with SRR1[3] will result in a 0, thus
keeping this bit stable.

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