[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 #10 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)
> that's a bug, yay!  spec - in the pseudo-code - is this:
> 
>     MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
>     MSR[3] <- (MSR[3] & SRR1[3])

Where do I find this and similar relevant pseudocode?  I've looked through the
wiki without success.  I've found a POWER9 ISA manual online, but it lacks
anything like the detail given above.  I've checked out the OpenPOWER ISA spec
3.0b that is linked from the wiki, and ... I have to admit I'm deeply flustered
by my inability to locate useful information in that document.

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